:: Coherent Space
::  by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies TARSKI, XBOOLE_0, CLASSES1, ZFMISC_1, EQREL_1, TOLER_1, SETFAM_1,
      SUBSET_1, FUNCT_2, FUNCT_1, RELAT_1, MCART_1, GRAPH_1, ENS_1, PARTFUN1,
      CAT_1, COH_SP, STRUCT_0, MONOID_0, RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1,
      MCART_1, FUNCT_1, PARTFUN1, CLASSES1, FUNCT_2, BINOP_1, EQREL_1, TOLER_1,
      STRUCT_0, GRAPH_1, CAT_1;
 constructors BINOP_1, EQREL_1, CLASSES1, TOLER_1, CAT_1, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      EQREL_1, CAT_2, RELAT_1, CAT_1, XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, CLASSES1, XBOOLE_0, BINOP_1, RELAT_1, CAT_1, GRAPH_1,
      XTUPLE_0;
 theorems TARSKI, ZFMISC_1, TOLER_1, ENUMSET1, RELAT_1, FUNCT_2, CLASSES1,
      PARTFUN1, MCART_1, FUNCT_1, DOMAIN_1, CAT_1, XBOOLE_0, XBOOLE_1, EQREL_1,
      XTUPLE_0;
 schemes TOLER_1, TARSKI, FUNCT_2, BINOP_1, XBOOLE_0;

begin

reserve x,y,z,a,b,c,X,A for set;

:: Coherent Space and Web of Coherent Space

definition
  let IT be set;

  attr IT is binary_complete means
  :Def1:
  for A st A c= IT & (for a,b st a in
  A & b in A holds a \/ b in IT) holds union A in IT;
end;

registration
  cluster subset-closed binary_complete non empty for set;
  existence
  proof
    take X={{}};
    thus for a,b st a in X & b c= a holds b in X
    proof
      let a,b;
      assume that
A1:   a in X and
A2:   b c= a;
      a = {} by A1,TARSKI:def 1;
      hence thesis by A1,A2;
    end;
    thus for A st A c= X & (for a,b st a in A & b in A holds a \/ b in X)
    holds union A in X
    proof
      let A such that
A3:   A c= X and
      for a,b st a in A & b in A holds a \/ b in X;
      now
        per cases by A3,ZFMISC_1:33;
        suppose
          A = {};
          hence thesis by TARSKI:def 1,ZFMISC_1:2;
        end;
        suppose
          A = {{}};
          then union A = {} by ZFMISC_1:25;
          hence thesis by TARSKI:def 1;
        end;
      end;
      hence thesis;
    end;
    thus thesis;
  end;
end;

definition
  mode Coherence_Space is subset-closed binary_complete non empty set;
end;

reserve C,D for Coherence_Space;

theorem
  {} in C
proof
  {} c= C & for a,b st a in {} & b in {} holds a \/ b in C by XBOOLE_1:2;
  hence thesis by Def1,ZFMISC_1:2;
end;

theorem Th2:
  bool X is Coherence_Space
proof
A1: for A st A c= bool X & (for a,b st a in A & b in A holds a \/ b in bool
  X) holds union A in bool X
  proof
    let A;
    assume that
A2: A c= bool X and
    for a,b st a in A & b in A holds a \/ b in bool X;
    for a st a in A holds a c= X by A2;
    then union A c= X by ZFMISC_1:76;
    hence thesis;
  end;
  for a, b st a in bool X & b c= a holds b in bool X
  proof
    let a,b;
    assume a in bool X & b c= a;
    then b c= X by XBOOLE_1:1;
    hence thesis;
  end;
  hence thesis by A1,Def1,CLASSES1:def 1;
end;

theorem
  {{}} is Coherence_Space by Th2,ZFMISC_1:1;

theorem Th4:
  x in union C implies {x} in C
proof
  assume x in union C;
  then consider X such that
A1: x in X and
A2: X in C by TARSKI:def 4;
  {x} c= X by A1,ZFMISC_1:31;
  hence thesis by A2,CLASSES1:def 1;
end;

definition
  let C be Coherence_Space;
  func Web(C) -> Tolerance of union C means
  :Def2:
  for x,y holds [x,y] in it iff ex X st X in C & x in X & y in X;
  existence
  proof
    defpred P[set,set] means ex X st X in C & $1 in X & $2 in X;
A1: for x st x in union C holds P[x,x]
    proof
      let x such that
A2:   x in union C;
      take {x};
      thus thesis by A2,Th4,TARSKI:def 1;
    end;
A3: for x,y st x in union C & y in union C & P[x,y] holds P[y,x];
    consider T be Tolerance of union C such that
A4: for x,y st x in union C & y in union C holds [x,y] in T iff P[x,y]
    from TOLER_1:sch 1(A1,A3);
    take T;
    let x,y;
    thus [x,y] in T implies ex X st X in C & x in X & y in X
    proof
      assume
A5:   [x,y] in T;
      then x in union C & y in union C by ZFMISC_1:87;
      hence thesis by A4,A5;
    end;
    given X such that
A6: X in C & x in X & y in X;
    x in union C & y in union C by A6,TARSKI:def 4;
    hence thesis by A4,A6;
  end;
  uniqueness by TOLER_1:25;
end;

reserve T for Tolerance of union C;

theorem Th5:
  T = Web(C) iff for x,y holds [x,y] in T iff {x,y} in C
proof
  thus T = Web(C) implies for x,y holds [x,y] in T iff {x,y} in C
  proof
    assume
A1: T = Web(C);
    let x,y;
    thus [x,y] in T implies {x,y} in C
    proof
      assume [x,y] in T;
      then consider X such that
A2:   X in C and
A3:   x in X & y in X by A1,Def2;
      {x,y} c= X by A3,ZFMISC_1:32;
      hence thesis by A2,CLASSES1:def 1;
    end;
A4: x in {x,y} & y in {x,y} by TARSKI:def 2;
    assume {x,y} in C;
    hence thesis by A1,A4,Def2;
  end;
  assume
A5: for x,y holds [x,y] in T iff {x,y} in C;
  for x,y holds [x,y] in T iff ex X st X in C & x in X & y in X
  proof
    let x,y;
    thus [x,y] in T implies ex X st X in C & x in X & y in X
    proof
      assume
A6:   [x,y] in T;
      take {x,y};
      thus thesis by A5,A6,TARSKI:def 2;
    end;
    given X such that
A7: X in C and
A8: x in X & y in X;
    {x,y} c= X by A8,ZFMISC_1:32;
    then {x,y} in C by A7,CLASSES1:def 1;
    hence thesis by A5;
  end;
  hence thesis by Def2;
end;

theorem Th6:
  a in C iff for x,y st x in a & y in a holds {x,y} in C
proof
  defpred P[set,set] means {$1} = $2;
  thus a in C implies for x,y st x in a & y in a holds {x,y} in C
  proof
    assume
A1: a in C;
    let x,y;
    assume x in a & y in a;
    then {x,y} c= a by ZFMISC_1:32;
    hence thesis by A1,CLASSES1:def 1;
  end;
A2: for x,y,z st P[x,y] & P[x,z] holds y = z;
  consider X such that
A3: for x holds x in X iff ex y st y in a & P[y,x] from TARSKI:sch 1(A2);
  assume
A4: for x,y st x in a & y in a holds {x,y} in C;
A5: for b,c st b in X & c in X holds b \/ c in C
  proof
    let b,c;
    assume that
A6: b in X and
A7: c in X;
    consider z such that
A8: z in a and
A9: {z} = c by A3,A7;
    consider y such that
A10: y in a and
A11: {y} = b by A3,A6;
    {y,z} in C by A4,A10,A8;
    hence thesis by A11,A9,ENUMSET1:1;
  end;
A12: union X = a
  proof
    thus union X c= a
    proof
      let x;
      assume x in union X;
      then consider Z be set such that
A13:  x in Z and
A14:  Z in X by TARSKI:def 4;
      ex y st y in a & Z = {y} by A3,A14;
      hence thesis by A13,TARSKI:def 1;
    end;
    let x;
    assume x in a;
    then
A15: {x} in X by A3;
    x in {x} by TARSKI:def 1;
    hence thesis by A15,TARSKI:def 4;
  end;
  X c= C
  proof
    let x;
    assume x in X;
    then consider y such that
A16: y in a and
A17: {y} = x by A3;
    {y,y} in C by A4,A16;
    hence thesis by A17,ENUMSET1:29;
  end;
  hence thesis by A5,A12,Def1;
end;

theorem Th7:
  a in C iff for x,y st x in a & y in a holds [x,y] in Web(C)
proof
  thus a in C implies for x,y st x in a & y in a holds [x,y] in Web(C)
  proof
    assume
A1: a in C;
    let x,y;
    assume x in a & y in a;
    then {x,y} in C by A1,Th6;
    hence thesis by Th5;
  end;
  assume
A2: for x,y st x in a & y in a holds [x,y] in Web(C);
  now
    let x,y;
    assume x in a & y in a;
    then [x,y] in Web(C) by A2;
    hence {x,y} in C by Th5;
  end;
  hence thesis by Th6;
end;

theorem
  (for x,y st x in a & y in a holds {x,y} in C) implies a c= union C
proof
  assume
A1: for x,y st x in a & y in a holds {x,y} in C;
  let x;
  assume x in a;
  then {x,x} in C by A1;
  then
A2: {x} in C by ENUMSET1:29;
  x in {x} by TARSKI:def 1;
  hence thesis by A2,TARSKI:def 4;
end;

theorem
  Web(C) = Web(D) implies C = D
proof
  assume
A1: Web(C) = Web(D);
  thus C c= D
  proof
    let x;
    assume x in C;
    then for z,y st z in x & y in x holds [z,y] in Web(D) by A1,Th7;
    hence thesis by Th7;
  end;
  let x;
  assume x in D;
  then for z,y st z in x & y in x holds [z,y] in Web(C) by A1,Th7;
  hence thesis by Th7;
end;

theorem
  union C in C implies C = bool union C
proof
  assume
A1: union C in C;
  thus C c= bool union C by ZFMISC_1:82;
  let x;
  assume x in bool union C;
  hence thesis by A1,CLASSES1:def 1;
end;

theorem
  C = bool union C implies Web(C) = Total union C
proof
  reconsider t = Total union C as Tolerance of union C;
  assume
A1: C = bool union C;
  now
    let x,y;
    thus [x,y] in t implies {x,y} in C
    proof
      assume [x,y] in t;
      then
A2:   x in union C & y in union C by ZFMISC_1:87;
      {x,y} c= union C
      proof
        let z;
        assume z in {x,y};
        hence thesis by A2,TARSKI:def 2;
      end;
      hence thesis by A1;
    end;
    assume {x,y} in C;
    then x in union C & y in union C by A1,ZFMISC_1:32;
    hence [x,y] in t by TOLER_1:2;
  end;
  hence thesis by Th5;
end;

definition
  let X be set;
  let E be Tolerance of X;
  func CohSp(E) -> Coherence_Space means
  :Def3:
  for a holds a in it iff for x, y st x in a & y in a holds [x,y] in E;
  existence
  proof
    defpred P[set] means for x,y st x in $1 & y in $1 holds [x,y] in E;
    consider Z be set such that
A1: for x holds x in Z iff x in bool X & P[x] from XBOOLE_0:sch 1;
A2: for A st A c= Z & (for a,b st a in A & b in A holds a \/ b in Z) holds
    union A in Z
    proof
      let A such that
A3:   A c= Z and
A4:   for a,b st a in A & b in A holds a \/ b in Z;
A5:   now
        let x,y;
        assume that
A6:     x in union A and
A7:     y in union A;
        consider Y1 be set such that
A8:     y in Y1 and
A9:     Y1 in A by A7,TARSKI:def 4;
        consider X1 be set such that
A10:    x in X1 and
A11:    X1 in A by A6,TARSKI:def 4;
A12:    x in X1 \/ Y1 by A10,XBOOLE_0:def 3;
A13:    y in X1 \/ Y1 by A8,XBOOLE_0:def 3;
        X1 \/ Y1 in Z by A4,A11,A9;
        hence [x,y] in E by A1,A12,A13;
      end;
      now
        let a;
        assume a in A;
        then a in bool X by A1,A3;
        hence a c= X;
      end;
      then union A c= X by ZFMISC_1:76;
      hence thesis by A1,A5;
    end;
A14: for a,b st a in Z & b c= a holds b in Z
    proof
      let a,b;
      assume that
A15:  a in Z and
A16:  b c= a;
      a in bool X by A1,A15;
      then
A17:  b c= X by A16,XBOOLE_1:1;
      for x,y st x in b & y in b holds [x,y] in E by A1,A15,A16;
      hence thesis by A1,A17;
    end;
    ( P[{}])& {} c= X by XBOOLE_1:2;
    then reconsider Z as Coherence_Space by A1,A14,A2,Def1,CLASSES1:def 1;
    take Z;
    let a;
    thus a in Z implies for x,y st x in a & y in a holds [x,y] in E by A1;
    assume
A18: for x,y st x in a & y in a holds [x,y] in E;
    then a c= X by TOLER_1:18,def 1;
    hence thesis by A1,A18;
  end;
  uniqueness
  proof
    let C,D;
    assume that
A19: for a holds a in C iff for x,y st x in a & y in a holds [x,y] in E and
A20: for a holds a in D iff for x,y st x in a & y in a holds [x,y] in E;
    thus C c= D
    proof
      let x;
      assume x in C;
      then for z,y st z in x & y in x holds [z,y] in E by A19;
      hence thesis by A20;
    end;
    let x;
    assume x in D;
    then for z,y st z in x & y in x holds [z,y] in E by A20;
    hence thesis by A19;
  end;
end;

reserve E for Tolerance of X;

theorem
  Web(CohSp(E)) = E
proof
  now
    let x,y;
    thus [x,y] in Web(CohSp(E)) implies [x,y] in E
    proof
      assume [x,y] in Web(CohSp(E));
      then
A1:   {x,y} in CohSp(E) by Th5;
      x in {x,y} & y in {x,y} by TARSKI:def 2;
      hence thesis by A1,Def3;
    end;
    assume
A2: [x,y] in E;
    then
A3: x in X & y in X by ZFMISC_1:87;
    for u,v be set st u in {x,y} & v in {x,y} holds [u,v] in E
    proof
      let u,v be set;
      assume that
A4:   u in {x,y} and
A5:   v in {x,y};
A6:   v = x or v = y by A5,TARSKI:def 2;
      u = x or u = y by A4,TARSKI:def 2;
      hence thesis by A2,A3,A6,EQREL_1:6,TOLER_1:7;
    end;
    then {x,y} in CohSp(E) by Def3;
    hence [x,y] in Web(CohSp(E)) by Th5;
  end;
  hence thesis by RELAT_1:def 2;
end;

theorem
  CohSp(Web(C)) = C
proof
  thus CohSp(Web(C)) c= C
  proof
    let x;
    assume x in CohSp(Web(C));
    then for y,z st y in x & z in x holds [y,z] in Web(C) by Def3;
    hence thesis by Th7;
  end;
  let x;
  assume x in C;
  then for y,z st y in x & z in x holds [y,z] in Web(C) by Th7;
  hence thesis by Def3;
end;

theorem Th14:
  a in CohSp(E) iff a is TolSet of E
proof
  thus a in CohSp(E) implies a is TolSet of E
  proof
    assume a in CohSp(E);
    then for x,y st x in a & y in a holds [x,y] in E by Def3;
    hence thesis by TOLER_1:def 1;
  end;
  assume a is TolSet of E;
  then for x,y st x in a & y in a holds [x,y] in E by TOLER_1:def 1;
  hence thesis by Def3;
end;

theorem
  CohSp(E) = TolSets E
proof
  thus CohSp(E) c= TolSets E
  proof
    let x;
    assume x in CohSp(E);
    then x is TolSet of E by Th14;
    hence thesis by TOLER_1:def 3;
  end;
  let x;
  assume x in TolSets E;
  then x is TolSet of E by TOLER_1:def 3;
  hence thesis by Th14;
end;

begin :: Category of Coherence Spaces

definition
  let X;
  func CSp(X) -> set equals
  { x where x is Subset-Family of X : x is
  Coherence_Space };
  coherence;
end;

registration
  let X;
  cluster CSp(X) -> non empty;
  coherence
  proof
    reconsider b = bool X as Subset-Family of X;
    set F = { x where x is Subset-Family of X: x is Coherence_Space };
    b is Coherence_Space by Th2;
    then b in F;
    hence thesis;
  end;
end;

registration
  let X be set;
  cluster -> subset-closed binary_complete non empty for Element of CSp(X);
  coherence
  proof
    let C be Element of CSp(X);
    C in { x where x is Subset-Family of X : x is Coherence_Space };
    then ex x be Subset-Family of X st C = x & x is Coherence_Space;
    hence thesis;
  end;
end;

reserve C,C1,C2 for Element of CSp(X);

theorem Th16:
  {x,y} in C implies x in union C & y in union C
proof
A1: {x} c= {x,y} & {y} c= {x,y} by ZFMISC_1:7;
A2: x in {x} & y in {y} by TARSKI:def 1;
  assume {x,y} in C;
  hence thesis by A1,A2,TARSKI:def 4;
end;

definition
  let X;

  func FuncsC(X) -> set equals
  union { Funcs(union x,union y) where x is
  Element of CSp(X), y is Element of CSp(X): not contradiction };
  coherence;
end;

registration
  let X;
  cluster FuncsC(X) -> non empty functional;
  coherence
  proof
    reconsider A = bool X as Subset-Family of X;
    A is Coherence_Space by Th2;
    then A in { x where x is Subset-Family of X: x is Coherence_Space};
    then reconsider A as Element of CSp(X);
    set F = { Funcs(union T,union TT) where T is Element of CSp(X), TT is
    Element of CSp(X): not contradiction };
    id union A in Funcs(union A,union A) & Funcs(union A,union A) in F by
FUNCT_2:9;
    then reconsider UF = union F as non empty set by TARSKI:def 4;
    now
      let f be set;
      assume f in UF;
      then consider C being set such that
A1:   f in C and
A2:   C in F by TARSKI:def 4;
      ex A,B be Element of CSp(X) st C = Funcs(union A,union B) by A2;
      hence f is Function by A1;
    end;
    hence thesis by FUNCT_1:def 13;
  end;
end;

reserve g for Element of FuncsC(X);

theorem Th17:
  x in FuncsC(X) iff ex C1,C2 st (union C2 = {} implies union C1 =
  {}) & x is Function of union C1,union C2
proof
  set F = { Funcs(union xx,union y) where xx is Element of CSp(X), y is
  Element of CSp(X): not contradiction };
  thus x in FuncsC(X) implies ex C1,C2 st (union C2 = {} implies union C1 = {}
  ) & x is Function of union C1,union C2
  proof
    assume x in FuncsC(X);
    then consider C being set such that
A1: x in C and
A2: C in F by TARSKI:def 4;
    consider A,B be Element of CSp(X) such that
A3: C = Funcs(union A,union B) by A2;
    take A,B;
    thus thesis by A1,A3,FUNCT_2:66;
  end;
  given A,B be Element of CSp(X) such that
A4: ( union B={} implies union A={})& x is Function of union A,union B;
A5: Funcs(union A,union B) in F;
  x in Funcs(union A,union B) by A4,FUNCT_2:8;
  hence thesis by A5,TARSKI:def 4;
end;

definition
  let X;
  func MapsC(X) -> set equals
  { [[C,CC],f] where C is Element of CSp(X), CC is
Element of CSp(X), f is Element of FuncsC(X) : (union CC = {} implies union C =
{}) & f is Function of union C,union CC & for x,y st {x,y} in C holds {f.x,f.y}
  in CC};
  coherence;
end;

registration
  let X;
  cluster MapsC(X) -> non empty;
  coherence
  proof
    set FV = { [[T,TT],f] where T is Element of CSp(X), TT is Element of CSp(X
    ), f is Element of FuncsC(X) : (union TT = {} implies union T = {} ) & f is
Function of union T,union TT & for x,y st {x,y} in T holds {f.x,f.y} in TT};
    now
      reconsider A = bool X as Subset-Family of X;
      A is Coherence_Space by Th2;
      then A in { xx where xx is Subset-Family of X: xx is Coherence_Space};
      then reconsider A as Element of CSp(X);
      set f = id union A;
      take m = [[A,A],f];
A1:   union A = {} implies union A = {};
      reconsider f as Element of FuncsC(X) by Th17;
      now
        let x,y;
        assume
A2:     {x,y} in A;
        then x in union A by Th16;
        then
A3:     f.x = x by FUNCT_1:18;
        y in union A by A2,Th16;
        hence {f.x,f.y} in A by A2,A3,FUNCT_1:18;
      end;
      hence m in FV by A1;
    end;
    hence thesis;
  end;
end;

reserve l,l1,l2,l3 for Element of MapsC(X);

theorem Th18:
  ex g,C1,C2 st l = [[C1,C2],g] & (union C2 = {} implies union C1
= {}) & g is Function of union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,
  g.y} in C2
proof
  l in {[[C1,C2],g]: (union C2={} implies union C1={}) & g is Function of
  union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,g.y} in C2};
  then
  ex C1,C2,g st l = [[C1,C2],g] & (union C2={} implies union C1={}) & g is
  Function of union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,g.y} in C2;
  hence thesis;
end;

theorem Th19:
  for f being Function of union C1,union C2 st (union C2={}
implies union C1={}) & (for x,y st {x,y} in C1 holds {f.x,f.y} in C2) holds [[
  C1,C2],f] in MapsC(X)
proof
  let f be Function of union C1,union C2;
  assume that
A1: union C2={} implies union C1={} and
A2: for x,y st {x,y} in C1 holds {f.x,f.y} in C2;
  reconsider f9 = f as Element of FuncsC(X) by A1,Th17;
  for x,y st {x,y} in C1 holds {f9.x,f9.y} in C2 by A2;
  hence thesis by A1;
end;

registration
  let X be set, l be Element of MapsC(X);
  cluster l`2 -> Function-like Relation-like;
  coherence
  proof
    consider g be Element of FuncsC(X), C1,C2 be Element of CSp(X) such that
W:  l = [[C1,C2],g] &
    ( union C2 = {} implies union C1 = {})& g is Function of union C1,union
    C2 & for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
     [[C1,C2],g]`2 = g;
    hence thesis by W;
  end;
end;

definition
  let X,l;
  func dom l -> Element of CSp(X) equals
  l`1`1;
  coherence
  proof
    consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
    union C2 = {} implies union C1 = {} and
    g is Function of union C1,union C2 and
    for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
    [C1,C2] = [[C1,C2],g]`1 & [C1,C2]`1 = C1;
    hence thesis by A1;
  end;
  func cod l -> Element of CSp(X) equals
  l`1`2;
  coherence
  proof
    consider g,C1,C2 such that
A2: l = [[C1,C2],g] and
    union C2 = {} implies union C1 = {} and
    g is Function of union C1,union C2 and
    for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
    [C1,C2] = [[C1,C2],g]`1 & [C1,C2]`2 = C2;
    hence thesis by A2;
  end;
end;

theorem Th20:
  l = [[dom l,cod l],l`2]
proof
  consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
  union C2 = {} implies union C1 = {} and
  g is Function of union C1,union C2 and
  for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
  [C1,C2] = [[C1,C2],g]`1;
  then l`1 = [dom l,cod l] by A1,MCART_1:8;
  hence thesis by A1,MCART_1:8;
end;

Lm1: l`2 = l1`2 & dom l = dom l1 & cod l = cod l1 implies l = l1
proof
  l = [[dom l,cod l],l`2] by Th20;
  hence thesis by Th20;
end;

definition
  let X,C;
  func id$ C -> Element of MapsC(X) equals
  [[C,C],id union C];
  coherence
  proof
    set f = id union C;
    now
      let x,y;
      assume
A1:   {x,y} in C;
      then x in union C by Th16;
      then
A2:   (id union C).x = x by FUNCT_1:18;
      y in union C by A1,Th16;
      hence {f.x,f.y} in C by A1,A2,FUNCT_1:18;
    end;
    hence thesis by Th19;
  end;
end;

Lm2: for x1,y1,x2,y2,x3,y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds x1 =
y1 & x2 = y2
proof
  let x1,y1,x2,y2,x3,y3 be set;
  assume [[x1,x2],x3] = [[y1,y2],y3];
  then [x1,x2] = [y1,y2] by XTUPLE_0:1;
  hence thesis by XTUPLE_0:1;
end;

theorem Th21:
  (union cod l <> {} or union dom l = {}) & l`2 is Function of
union dom l,union cod l & for x,y st {x,y} in dom l holds {l`2.x,l`2.y} in cod
  l
proof
  consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
A2: ( union C2={} implies union C1 = {})& g is Function of union C1,
  union C2 and
A3: for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
A4: l = [[dom l,cod l],l`2] by Th20;
  then
A5: C2 = cod l by A1,Lm2;
A6: g = l`2 & C1 = dom l by A1,A4,Lm2,XTUPLE_0:1;
  hence (union cod l <> {} or union dom l = {}) & l`2 is Function of union dom
  l,union cod l by A1,A2,A4,Lm2;
  let x,y;
  assume {x,y} in dom l;
  hence thesis by A3,A6,A5;
end;

definition
  let X,l1,l2;
  assume
A1: cod l1 = dom l2;
  func l2*l1 -> Element of MapsC(X) equals
  :Def10:
  [[dom l1,cod l2],l2`2*l1`2];
  coherence
  proof
A2: union cod l2 <> {} or union dom l2 = {} by Th21;
A3: union cod l1 <> {} or union dom l1 = {} by Th21;
A4: l1`2 is Function of union dom l1,union cod l1 by Th21;
A5: now
      let x,y;
      assume
A6:   {x,y} in dom l1;
      then x in union dom l1 by Th16;
      then
A7:   x in dom l1`2 by A3,A4,FUNCT_2:def 1;
      y in union dom l1 by A6,Th16;
      then
A8:   y in dom l1`2 by A3,A4,FUNCT_2:def 1;
      {l1`2.x,l1`2.y} in cod l1 by A6,Th21;
      then {l2`2.(l1`2.x),l2`2.(l1`2.y)} in cod l2 by A1,Th21;
      then {(l2`2*l1`2).x,l2`2.(l1`2.y)} in cod l2 by A7,FUNCT_1:13;
      hence {(l2`2*l1`2).x,(l2`2*l1`2).y} in cod l2 by A8,FUNCT_1:13;
    end;
    l2`2 is Function of union dom l2,union cod l2 by Th21;
    then l2`2*l1`2 is Function of union dom l1,union cod l2 by A1,A3,A4,
FUNCT_2:13;
    hence thesis by A1,A3,A2,A5,Th19;
  end;
end;

theorem Th22:
  dom l2 = cod l1 implies (l2*l1)`2 = l2`2*l1`2 & dom(l2*l1) = dom
  l1 & cod(l2*l1) = cod l2
proof
  assume dom l2 = cod l1;
  then [[dom l1,cod l2],l2`2*l1`2] = l2*l1 by Def10
    .= [[dom(l2*l1),cod(l2*l1)],(l2*l1)`2] by Th20;
  hence thesis by Lm2,XTUPLE_0:1;
end;

theorem Th23:
  dom l2 = cod l1 & dom l3 = cod l2 implies l3*(l2*l1) = (l3*l2)* l1
proof
  assume that
A1: dom l2 = cod l1 and
A2: dom l3 = cod l2;
A3: cod(l2*l1) = cod l2 by A1,Th22;
  (l2*l1)`2 = l2`2*l1`2 by A1,Th22;
  then
A4: (l3*(l2*l1))`2 = l3`2*(l2`2*l1`2) by A2,A3,Th22;
A5: dom(l3*l2) = dom l2 by A2,Th22;
  then
A6: dom((l3*l2)*l1) = dom l1 by A1,Th22;
  dom(l2*l1) = dom l1 by A1,Th22;
  then
A7: dom(l3*(l2*l1)) = dom l1 by A2,A3,Th22;
  cod(l3*l2) = cod l3 by A2,Th22;
  then
A8: cod((l3*l2)*l1) = cod l3 by A1,A5,Th22;
  (l3*l2)`2 = l3`2*l2`2 by A2,Th22;
  then
A9: ((l3*l2)*l1)`2 = (l3`2*l2`2)*l1`2 by A1,A5,Th22;
  cod(l3*(l2*l1)) = cod l3 by A2,A3,Th22;
  hence thesis by A4,A7,A9,A6,A8,Lm1,RELAT_1:36;
end;

theorem Th24:
  (id$ C)`2 = id union C & dom id$ C = C & cod id$ C = C
proof
  [[dom id$ C,cod id$ C],(id$ C)`2] = [[C,C],id union C] by Th20;
  hence thesis by Lm2,XTUPLE_0:1;
end;

theorem Th25:
  l*(id$ dom l) = l & (id$ cod l)*l = l
proof
  set i1 = id$ dom l, i2 = id$ cod l;
A1: i1`2 = id union dom l & dom i1 = dom l by Th24;
A2: l`2 is Function of union dom l,union cod l by Th21;
  then
A3: rng l`2 c= union cod l by RELAT_1:def 19;
  union cod l <> {} or union dom l = {} by Th21;
  then
A4: dom l`2 = union dom l by A2,FUNCT_2:def 1;
A5: cod i1 = dom l by Th24;
  then
A6: cod(l*i1) = cod l by Th22;
  (l*i1)`2 = l`2*i1`2 & dom(l*i1) = dom i1 by A5,Th22;
  hence l*i1 = l by A4,A1,A6,Lm1,RELAT_1:52;
A7: i2`2 = id union cod l & cod i2 = cod l by Th24;
A8: dom i2 = cod l by Th24;
  then
A9: cod(i2*l) = cod i2 by Th22;
  (i2*l)`2 = i2`2*l`2 & dom(i2*l) = dom l by A8,Th22;
  hence thesis by A3,A7,A9,Lm1,RELAT_1:53;
end;

definition
  let X;
  func CDom X -> Function of MapsC(X),CSp(X) means
  :Def11:
  for l holds it.l = dom l;
  existence
  proof
    deffunc F(Element of MapsC(X)) = dom $1;
    thus ex f being Function of MapsC(X),CSp(X) st for x being Element of
    MapsC(X) holds f.x = F(x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let h1,h2 be Function of MapsC(X),CSp(X) such that
A1: for l holds h1.l = dom l and
A2: for l holds h2.l = dom l;
    now
      let l;
      thus h1.l = dom l by A1
        .= h2.l by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func CCod X -> Function of MapsC(X),CSp(X) means
  :Def12:
  for l holds it.l = cod l;
  existence
  proof
    deffunc F(Element of MapsC(X)) = cod $1;
    thus ex f being Function of MapsC(X),CSp(X) st for x being Element of
    MapsC(X) holds f.x = F(x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let h1,h2 be Function of MapsC(X),CSp(X) such that
A3: for l holds h1.l = cod l and
A4: for l holds h2.l = cod l;
    now
      let l;
      thus h1.l = cod l by A3
        .= h2.l by A4;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func CComp X -> PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) means
  :Def13:
  (for l2,l1 holds [l2,l1] in dom it iff dom l2 = cod l1) &
   for l2,l1 st dom l2 = cod l1 holds it.[l2,l1] = l2*l1;
  existence
  proof
    defpred P[set,set,set] means for l2,l1 st l2=$1 & l1=$2 holds dom l2 = cod
    l1 & $3 = l2*l1;
A5: for x,y,z1,z2 being set st x in MapsC(X) & y in MapsC(X) & P[x,y,z1]
    & P[x,y,z2] holds z1 = z2
    proof
      let x,y,z1,z2 be set;
      assume x in MapsC(X) & y in MapsC(X);
      then reconsider l2 = x, l1 = y as Element of MapsC(X);
      assume that
A6:   P[x,y,z1] and
A7:   P[x,y,z2];
      z1 = l2*l1 by A6;
      hence thesis by A7;
    end;
A8: for x,y,z being set st x in MapsC(X) & y in MapsC(X) & P[x,y,z] holds
    z in MapsC(X)
    proof
      let x,y,z be set;
      assume x in MapsC(X) & y in MapsC(X);
      then reconsider l2 = x, l1 = y as Element of MapsC(X);
      assume P[x,y,z];
      then z = l2*l1;
      hence thesis;
    end;
    consider h being PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) such that
A9: for x,y holds [x,y] in dom h iff x in MapsC(X) & y in MapsC(X) &
    ex z st P[x,y,z] and
A10: for x,y st [x,y] in dom h holds P[x,y,h.(x,y)] from BINOP_1:sch 5
    (A8, A5);
    take h;
    thus
A11: for l2,l1 holds [l2,l1] in dom h iff dom l2 = cod l1
    proof
      let l2,l1;
      thus [l2,l1] in dom h implies dom l2 = cod l1
      proof
        assume [l2,l1] in dom h;
        then ex z being set st P[l2,l1,z] by A9;
        hence thesis;
      end;
      assume dom l2 = cod l1;
      then P[l2,l1,l2*l1];
      hence thesis by A9;
    end;
    let l2,l1;
    assume dom l2 = cod l1;
    then [l2,l1] in dom h by A11;
    then P[l2,l1,h.(l2,l1)] by A10;
    hence thesis;
  end;
  uniqueness
  proof
    let h1,h2 be PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) such that
A12: for l2,l1 holds [l2,l1] in dom h1 iff dom l2 = cod l1 and
A13: for l2,l1 st dom l2 = cod l1 holds h1.[l2,l1] = l2*l1 and
A14: for l2,l1 holds [l2,l1] in dom h2 iff dom l2 = cod l1 and
A15: for l2,l1 st dom l2 = cod l1 holds h2.[l2,l1] = l2*l1;
A16: dom h1 = dom h2
    proof
      let x,y be set;
      thus [x,y] in dom h1 implies [x,y] in dom h2
      proof
        assume
A17:    [x,y] in dom h1;
        then reconsider l2 = x, l1 = y as Element of MapsC(X) by ZFMISC_1:87;
        dom l2 = cod l1 by A12,A17;
        hence thesis by A14;
      end;
      assume
A18:  [x,y] in dom h2;
      then reconsider l2 = x, l1 = y as Element of MapsC(X) by ZFMISC_1:87;
      dom l2 = cod l1 by A14,A18;
      hence thesis by A12;
    end;
    now
      let l be Element of [:MapsC(X),MapsC(X):] such that
A19:  l in dom h1;
      consider l2,l1 be Element of MapsC(X) such that
A20:  l = [l2,l1] by DOMAIN_1:1;
A21:  dom l2 = cod l1 by A12,A19,A20;
      then h1.[l2,l1] = l2*l1 by A13;
      hence h1.l = h2.l by A15,A20,A21;
    end;
    hence thesis by A16,PARTFUN1:5;
  end;
end;

canceled;

definition
 canceled;
  let X;
  func CohCat(X) -> non empty non void strict CatStr equals
  CatStr(# CSp(X),MapsC(X),CDom X,CCod X,CComp X #);
  coherence;
end;

registration let X;
 cluster CohCat X -> Category-like transitive associative reflexive;
 coherence
  proof
   set M = MapsC(X), d = CDom X, c = CCod X, p = CComp X;
   set C = CohCat X;
  thus
P1:  C is Category-like
   proof
    let ff,gg be Morphism of C;
     reconsider f=ff, g=gg as Element of M;
   d.gg = dom g & c.ff = cod f by Def11,Def12;
   hence thesis by Def13;
  end;
  thus
P2: C is transitive
   proof
     let ff,gg be Morphism of C such that
A1:   dom gg=cod ff;
      [gg,ff] in dom the Comp of C by A1,P1,CAT_1:def 6;
      then
U:    (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
      reconsider f=ff, g=gg as Element of M;
A2:   d.g = dom g & c.f = cod f by Def11,Def12;
      then
A3:   p.[g,f] = g*f by A1,Def13;
A4:   d.f = dom f & c.g = cod g by Def11,Def12;
      dom(g*f) = dom f & cod(g*f) = cod g by A1,A2,Th22;
      hence thesis by A3,A4,Def11,Def12,U;
    end;
thus
  C is associative
   proof
     let ff,gg,hh be Morphism of C such that
A5:   dom hh = cod gg and
A6:   dom gg = cod ff;
      reconsider f=ff, g=gg, h=hh as Element of M;
A7:   dom h = d.h & cod g = c.g by Def11,Def12;
      then
A8:   dom(h*g) = dom g by A5,Th22;
A9:   dom g = d.g & cod f = c.f by Def11,Def12;
      then
A10:  cod(g*f) = dom h by A5,A6,A7,Th22;
       [hh,gg] in dom the Comp of C by P1,CAT_1:def 6,A5;
       then
X2:    hh(*)gg =(the Comp of C).(hh,gg) by CAT_1:def 1;
       dom(hh(*)gg) = dom gg by P2,CAT_1:def 7,A5;
       then
X3:     [hh(*)gg,ff] in dom the Comp of C by P1,CAT_1:def 6,A6;
       [gg,ff] in dom the Comp of C by P1,CAT_1:def 6,A6;
       then
X1:    gg(*)ff =(the Comp of C).(gg,ff) by CAT_1:def 1;
       cod(gg(*)ff) = cod gg by P2,CAT_1:def 7,A6;
       then [hh,gg(*)ff] in dom the Comp of C by P1,CAT_1:def 6,A5;
      hence hh(*)(gg(*)ff)
         = (the Comp of C).(hh,(the Comp of C).(gg,ff)) by X1,CAT_1:def 1
        .= p.[h,g*f] by A6,A9,Def13
        .= h*(g*f) by A10,Def13
        .= (h*g)*f by A5,A6,A7,A9,Th23
        .= p.[h*g,f] by A6,A9,A8,Def13
        .= (the Comp of C).((the Comp of C).(hh,gg),ff) by A5,A7,Def13
        .= hh(*)gg(*)ff by X2,X3,CAT_1:def 1;
   end;
    let a be Object of C;
     reconsider aa = a as Element of CSp X;
     reconsider ii = id$ aa as Morphism of C;

A12: cod ii = cod id$ aa by Def12 .= aa by Th24;
     dom ii = dom id$ aa by Def11 .= aa by Th24;
     then id$ aa in Hom(a,a) by A12;
    hence Hom(a,a)<>{};
  end;
end;

LmX:
  for a being Element of CohCat X, aa being Element of CSp X st a = aa
  for i being Morphism of a,a st i = id$ aa
  for b being Element of CohCat X holds
   (Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
   (Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
  proof let a be Element of CohCat X, aa be Element of CSp X such that
Z1: a = aa;
   let i be Morphism of a,a such that
Z2: i = id$ aa;
  let b be Element of CohCat X;
  thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
   proof assume
Z3:  Hom(a,b)<>{};
    let g be Morphism of a,b;
     reconsider gg = g as Element of MapsC X;
     Hom(a,a)<>{};
     then
A1:  cod i = a by CAT_1:5 .= dom g by Z3,CAT_1:5;
A3:  dom gg = dom g by Def11 .= aa by Z1,Z3,CAT_1:5;
     then
A2:  cod id$ aa = dom gg by Th24;
     [g,i] in dom the Comp of CohCat X by A1,CAT_1:def 6;
    hence g(*)i = (the Comp of CohCat X).(g,i) by CAT_1:def 1
       .= gg*id$ aa by A2,Z2,Def13
       .= g by A3,Th25;
   end;
   thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
   proof assume
Z3:  Hom(b,a)<>{};
    let g be Morphism of b,a;
     reconsider gg = g as Element of MapsC X;
     Hom(a,a)<>{};
     then
A1:  dom i = a by CAT_1:5 .= cod g by Z3,CAT_1:5;
A3:  cod gg = cod g by Def12 .= aa by Z1,Z3,CAT_1:5;
     then
A2:  dom id$ aa = cod gg by Th24;
     [i,g] in dom the Comp of CohCat X by A1,CAT_1:def 6;
    hence i(*)g = (the Comp of CohCat X).(i,g) by CAT_1:def 1
       .= (id$ aa)*gg by Z2,A2,Def13
       .= g by A3,Th25;
   end;
  end;

registration let X;
 cluster CohCat X -> with_identities;
 coherence
  proof let a being Element of CohCat X;
    reconsider aa = a as Element of CSp X;
    reconsider ii = id$ aa as Morphism of CohCat X;
A12: cod ii = cod id$ aa by Def12 .= aa by Th24;
     dom ii = dom id$ aa by Def11 .= aa by Th24;
    then ii in Hom(a,a) by A12;
    then reconsider ii as Morphism of a,a by CAT_1:def 5;
   take ii;
   thus thesis by LmX;
  end;
end;

begin :: Category of Tolerances

definition
  let X be set;
  func Toler(X) -> set means
  :Def16:
  x in it iff x is Tolerance of X;
  existence
  proof
    defpred P[set] means $1 is Tolerance of X;
    consider a such that
A1: for x holds x in a iff x in bool [:X,X:] & P[x] from XBOOLE_0:sch
    1;
    take a;
    let x;
    thus x in a implies x is Tolerance of X by A1;
    assume x is Tolerance of X;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let a,b be set;
    assume that
A2: x in a iff x is Tolerance of X and
A3: x in b iff x is Tolerance of X;
    now
      let x;
A4:   now
        assume x in b;
        then x is Tolerance of X by A3;
        hence x in a by A2;
      end;
      now
        assume x in a;
        then x is Tolerance of X by A2;
        hence x in b by A3;
      end;
      hence x in a iff x in b by A4;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let X be set;
  cluster Toler(X) -> non empty;
  coherence
  proof
    set T = the Tolerance of X;
    T in Toler X by Def16;
    hence thesis;
  end;
end;

definition
  let X be set;
  func Toler_on_subsets(X) -> set equals
  union {Toler(Y) where Y is Subset of
X: not contradiction};
  coherence;
end;

registration
  let X be set;
  cluster Toler_on_subsets(X) -> non empty;
  coherence
  proof
    set F = {Toler(Y) where Y is Subset of X: not contradiction};
    {} c= X by XBOOLE_1:2;
    then
A1: Toler({}) in F;
    {} in Toler({}) by Def16,TOLER_1:14;
    hence thesis by A1,TARSKI:def 4;
  end;
end;

theorem
  x in Toler_on_subsets(X) iff ex A st A c= X & x is Tolerance of A
proof
  set f = {Toler(Y) where Y is Subset of X: not contradiction};
  thus x in Toler_on_subsets(X) implies ex A st A c= X & x is Tolerance of A
  proof
    assume x in Toler_on_subsets(X);
    then consider a such that
A1: x in a and
A2: a in f by TARSKI:def 4;
    consider Y be Subset of X such that
A3: a = Toler(Y) by A2;
    take Y;
    thus thesis by A1,A3,Def16;
  end;
  given A such that
A4: A c= X and
A5: x is Tolerance of A;
  reconsider A as Subset of X by A4;
A6: Toler(A) in f;
  x in Toler(A) by A5,Def16;
  hence thesis by A6,TARSKI:def 4;
end;

theorem
  Total a in Toler(a) by Def16;

theorem Th29:
  {} in Toler_on_subsets(X)
proof
  set F = {Toler(Y) where Y is Subset of X: not contradiction};
  {} c= X by XBOOLE_1:2;
  then
A1: Toler({}) in F;
  {} in Toler({}) by Def16,TOLER_1:14;
  hence thesis by A1,TARSKI:def 4;
end;

theorem Th30:
  a c= X implies Total a in Toler_on_subsets(X)
proof
  set F = {Toler(Y) where Y is Subset of X: not contradiction};
  assume a c= X;
  then
A1: Toler(a) in F;
  Total a in Toler(a) by Def16;
  hence thesis by A1,TARSKI:def 4;
end;

theorem Th31:
  a c= X implies id a in Toler_on_subsets(X)
proof
  set F = {Toler(Y) where Y is Subset of X: not contradiction};
  assume a c= X;
  then
A1: Toler(a) in F;
  id a in Toler(a) by Def16;
  hence thesis by A1,TARSKI:def 4;
end;

theorem
  Total X in Toler_on_subsets(X) by Th30;

theorem
  id X in Toler_on_subsets(X) by Th31;

definition
  let X;
  func TOL(X) -> set equals
  { [t,Y] where t is Element of Toler_on_subsets(X),
  Y is Subset of X : t is Tolerance of Y};
  coherence;
end;

registration
  let X;
  cluster TOL(X) -> non empty;
  coherence
  proof
    set FV = { [t,Y] where t is Element of Toler_on_subsets(X), Y is Subset of
X:  t is Tolerance of Y};
    now
      reconsider o = {} as Subset of X by XBOOLE_1:2;
      reconsider e = {} as Element of Toler_on_subsets(X) by Th29;
      take m = [e,o];
      thus m in FV by TOLER_1:14;
    end;
    hence thesis;
  end;
end;

reserve T,T1,T2 for Element of TOL(X);

theorem
  [{},{}] in TOL(X)
proof
  {} in Toler_on_subsets(X) & {} c= X by Th29,XBOOLE_1:2;
  hence thesis by TOLER_1:14;
end;

theorem Th35:
  a c= X implies [id a,a] in TOL(X)
proof
  assume
A1: a c= X;
  then id a in Toler_on_subsets(X) by Th31;
  hence thesis by A1;
end;

theorem Th36:
  a c= X implies [Total a,a] in TOL(X)
proof
  assume
A1: a c= X;
  then Total a in Toler_on_subsets(X) by Th30;
  hence thesis by A1;
end;

theorem
  [id X,X] in TOL(X) by Th35;

theorem
  [Total X,X] in TOL(X) by Th36;

definition
  let X,T;
  redefine func T`2 -> Subset of X;
  coherence
  proof
    T in { [t,Y] where t is Element of Toler_on_subsets(X), Y is Subset of
X:  t is Tolerance of Y};
    then consider t be Element of Toler_on_subsets(X),Y be Subset of X
    such that
W:   T = [t,Y] & t is Tolerance of Y;
    [t,Y]`2 = Y;
    hence thesis by W;
  end;
  redefine func T`1 -> Tolerance of T`2;
  coherence
  proof
    T in { [t,Y] where t is Element of Toler_on_subsets(X), Y is Subset of
X:  t is Tolerance of Y};
    then consider
    t be Element of Toler_on_subsets(X),Y be Subset of X such that
A1: T = [t,Y] and
A2: t is Tolerance of Y;
    [t,Y]`2 = Y & [t,Y]`1 = t;
    hence thesis by A1,A2;
  end;
end;

definition
  let X;
  func FuncsT(X) -> set equals
  union { Funcs(T`2,TT`2) where T is Element of
  TOL(X), TT is Element of TOL(X): not contradiction };
  coherence;
end;

registration
  let X;
  cluster FuncsT(X) -> non empty functional;
  coherence
  proof
    set F = { Funcs(T`2,TT`2) where T is Element of TOL(X), TT is Element of
    TOL(X): not contradiction };
    reconsider T = [Total {}X,{}X] as Element of TOL(X) by Th36;
    [Total {}X,{}X]`2 = {}X;
    then
A1: id {}X in Funcs(T`2,T`2) by FUNCT_2:9;
    Funcs(T`2,T`2) in F;
    then reconsider UF = union F as non empty set by A1,TARSKI:def 4;
    now
      let f be set;
      assume f in UF;
      then consider C being set such that
A2:   f in C and
A3:   C in F by TARSKI:def 4;
      ex A,B be Element of TOL(X) st C = Funcs(A`2,B`2) by A3;
      hence f is Function by A2;
    end;
    hence thesis by FUNCT_1:def 13;
  end;
end;

reserve f for Element of FuncsT(X);

theorem Th39:
  x in FuncsT(X) iff ex T1,T2 st (T2`2 = {} implies T1`2 = {}) & x
  is Function of T1`2,T2`2
proof
  set F = { Funcs(T`2,TT`2) where T is Element of TOL(X), TT is Element of TOL
  (X): not contradiction };
  thus x in FuncsT(X) implies ex A,B be Element of TOL(X) st (B`2={} implies A
  `2={}) & x is Function of A`2,B`2
  proof
    assume x in FuncsT(X);
    then consider C being set such that
A1: x in C and
A2: C in F by TARSKI:def 4;
    consider A,B be Element of TOL(X) such that
A3: C = Funcs(A`2,B`2) by A2;
    take A,B;
    thus thesis by A1,A3,FUNCT_2:66;
  end;
  given A,B be Element of TOL(X) such that
A4: ( B`2={} implies A`2={})& x is Function of A`2,B`2;
A5: Funcs(A`2,B`2) in F;
  x in Funcs(A`2,B`2) by A4,FUNCT_2:8;
  hence thesis by A5,TARSKI:def 4;
end;

definition
  let X;
  func MapsT(X) -> set equals
  { [[T,TT],f] where T is Element of TOL(X), TT is
Element of TOL(X), f is Element of FuncsT(X) : (TT`2 = {} implies T`2 = {}) & f
  is Function of T`2,TT`2 & for x,y st [x,y] in T`1 holds [f.x,f.y] in TT`1};
  coherence;
end;

registration
  let X;
  cluster MapsT(X) -> non empty;
  coherence
  proof
    set FV = { [[T,TT],f] where T is Element of TOL(X), TT is Element of TOL(X
), f is Element of FuncsT(X) : (TT`2 = {} implies T`2 = {}) & f is Function of
    T`2,TT`2 & for x,y st [x,y] in T`1 holds [f.x,f.y] in TT`1};
    now
      set a = [Total {}X,{}X], f = id a`2;
      take m = [[a,a],f];
      reconsider a as Element of TOL(X) by Th36;
   a`2 = {} implies a`2 = {};
      then reconsider f as Element of FuncsT(X) by Th39;
      for x,y st [x,y] in a`1 holds [f.x,f.y] in a`1;
     hence m in FV;
    end;
    hence thesis;
  end;
end;

reserve m,m1,m2,m3 for Element of MapsT(X);

theorem Th40:
  ex f,T1,T2 st m = [[T1,T2],f] & (T2`2 = {} implies T1`2 = {}) &
  f is Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1
proof
  m in {[[T1,T2],f]: (T2`2={} implies T1`2={}) & f is Function of T1`2,T2
  `2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1};
  then ex T1,T2,f st m = [[T1,T2],f] & (T2`2={} implies T1`2={}) & f is
  Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1;
  hence thesis;
end;

theorem Th41:
  for f being Function of T1`2,T2`2 st (T2`2={} implies T1`2={}) &
(for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1) holds [[T1,T2],f] in MapsT(X
  )
proof
  let f be Function of T1`2,T2`2;
  assume that
A1: T2`2={} implies T1`2={} and
A2: for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1;
  reconsider f9 = f as Element of FuncsT(X) by A1,Th39;
  for x,y st [x,y] in T1`1 holds [f9.x,f9.y] in T2`1 by A2;
  hence thesis by A1;
end;

registration
  let X be set,m be Element of MapsT(X);
  cluster m`2 -> Function-like Relation-like;
  coherence
  proof
    consider f be Element of FuncsT(X), T1,T2 be Element of TOL(X) such that
W:    m = [[T1,T2],f] &
      ( T2`2 = {} implies T1`2 = {})& f is Function of T1`2,T2`2 & for x,y st [
    x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th40;
    [[T1,T2],f]`2 =f;
    hence thesis by W;
  end;
end;

definition
  let X,m;

  func dom m -> Element of TOL(X) equals
  m`1`1;
  coherence
  proof
    consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
    T2`2 = {} implies T1`2 = {} and
    f is Function of T1`2,T2`2 and
    for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th40;
    [T1,T2] = [[T1,T2],f]`1 & [T1,T2]`1 = T1;
    hence thesis by A1;
  end;
  func cod m -> Element of TOL(X) equals
  m`1`2;
  coherence
  proof
    consider f be Element of FuncsT(X),T1,T2 such that
A2: m = [[T1,T2],f] and
    T2`2 = {} implies T1`2 = {} and
    f is Function of T1`2,T2`2 and
    for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th40;
    [T1,T2] = [[T1,T2],f]`1 & [T1,T2]`2 = T2;
    hence thesis by A2;
  end;
end;

theorem Th42:
  m = [[dom m,cod m],m`2]
proof
  consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
  T2`2 = {} implies T1`2 = {} and
  f is Function of T1`2,T2`2 and
  for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th40;
  [T1,T2] = [[T1,T2],f]`1;
  then m`1 = [dom m,cod m] by A1,MCART_1:8;
  hence thesis by A1,MCART_1:8;
end;

Lm3: m`2 = m1`2 & dom m = dom m1 & cod m = cod m1 implies m = m1
proof
  m = [[dom m,cod m],m`2] by Th42;
  hence thesis by Th42;
end;

definition
  let X,T;
  func id$ T -> Element of MapsT(X) equals
  [[T,T],id T`2];
  coherence
  proof
    set f = id T`2;
    now
      let x,y;
      assume
A1:   [x,y] in T`1;
      then x in T`2 by ZFMISC_1:87;
      then
A2:   (id T`2).x = x by FUNCT_1:18;
      y in T`2 by A1,ZFMISC_1:87;
      hence [f.x,f.y] in T`1 by A1,A2,FUNCT_1:18;
    end;
    hence thesis by Th41;
  end;
end;

theorem Th43:
  ((cod m)`2 <> {} or (dom m)`2 = {}) & m`2 is Function of (dom m)
  `2,(cod m)`2 & for x,y st [x,y] in (dom m)`1 holds [m`2.x,m`2.y] in (cod m)`1
proof
  consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
A2: ( T2`2 = {} implies T1`2 = {})& f is Function of T1`2,T2`2 and
A3: for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th40;
A4: m = [[dom m,cod m],m`2] by Th42;
  then
A5: T2 = cod m by A1,Lm2;
A6: f = m`2 & T1 = dom m by A1,A4,Lm2,XTUPLE_0:1;
  hence
  ((cod m)`2<>{} or (dom m)`2={} ) & m`2 is Function of (dom m)`2,(cod m)
  `2 by A1,A2,A4,Lm2;
  let x,y;
  assume [x,y] in (dom m)`1;
  hence thesis by A3,A6,A5;
end;

definition
  let X,m1,m2;
  assume
A1: cod m1 = dom m2;
  func m2*m1 -> Element of MapsT(X) equals
  :Def24:
  [[dom m1,cod m2],m2`2*m1`2];
  coherence
  proof
A2: (cod m2)`2 <> {} or (dom m2)`2 = {} by Th43;
A3: (cod m1)`2 <> {} or (dom m1)`2 = {} by Th43;
A4: m1`2 is Function of (dom m1)`2,(cod m1)`2 by Th43;
A5: now
      let x,y;
      assume
A6:   [x,y] in (dom m1)`1;
      then x in (dom m1)`2 by ZFMISC_1:87;
      then
A7:   x in dom m1`2 by A3,A4,FUNCT_2:def 1;
      y in (dom m1)`2 by A6,ZFMISC_1:87;
      then
A8:   y in dom m1`2 by A3,A4,FUNCT_2:def 1;
      [m1`2.x,m1`2.y] in (cod m1)`1 by A6,Th43;
      then [m2`2.(m1`2.x),m2`2.(m1`2.y)] in (cod m2)`1 by A1,Th43;
      then [(m2`2*m1`2).x,m2`2.(m1`2.y)] in (cod m2)`1 by A7,FUNCT_1:13;
      hence [(m2`2*m1`2).x,(m2`2*m1`2).y] in (cod m2)`1 by A8,FUNCT_1:13;
    end;
    m2`2 is Function of (dom m2)`2,(cod m2)`2 by Th43;
    then m2`2*m1`2 is Function of (dom m1)`2,(cod m2)`2 by A1,A3,A4,FUNCT_2:13;
    hence thesis by A1,A3,A2,A5,Th41;
  end;
end;

theorem Th44:
  dom m2 = cod m1 implies (m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom
  m1 & cod(m2*m1) = cod m2
proof
  assume dom m2 = cod m1;
  then [[dom m1,cod m2],m2`2*m1`2] = m2*m1 by Def24
    .= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th42;
  hence thesis by Lm2,XTUPLE_0:1;
end;

theorem Th45:
  dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)* m1
proof
  assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2;
A3: cod(m2*m1) = cod m2 by A1,Th44;
  (m2*m1)`2 = m2`2*m1`2 by A1,Th44;
  then
A4: (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) by A2,A3,Th44;
A5: dom(m3*m2) = dom m2 by A2,Th44;
  then
A6: dom((m3*m2)*m1) = dom m1 by A1,Th44;
  dom(m2*m1) = dom m1 by A1,Th44;
  then
A7: dom(m3*(m2*m1)) = dom m1 by A2,A3,Th44;
  cod(m3*m2) = cod m3 by A2,Th44;
  then
A8: cod((m3*m2)*m1) = cod m3 by A1,A5,Th44;
  (m3*m2)`2 = m3`2*m2`2 by A2,Th44;
  then
A9: ((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 by A1,A5,Th44;
  cod(m3*(m2*m1)) = cod m3 by A2,A3,Th44;
  hence thesis by A4,A7,A9,A6,A8,Lm3,RELAT_1:36;
end;

theorem Th46:
  (id$ T)`2 = id T`2 & dom id$ T = T & cod id$ T = T
proof
  [[dom id$ T,cod id$ T],(id$ T)`2] = [[T,T],id T`2] by Th42;
  hence thesis by Lm2,XTUPLE_0:1;
end;

theorem Th47:
  m*(id$ dom m) = m & (id$ cod m)*m = m
proof
  set i1 = id$ dom m, i2 = id$ cod m;
A1: i1`2 = id (dom m)`2 & dom i1 = dom m by Th46;
A2: m`2 is Function of (dom m)`2,(cod m)`2 by Th43;
  then
A3: rng m`2 c= (cod m)`2 by RELAT_1:def 19;
  (cod m)`2 <> {} or (dom m)`2 = {} by Th43;
  then
A4: dom m`2 = (dom m)`2 by A2,FUNCT_2:def 1;
A5: cod i1 = dom m by Th46;
  then
A6: cod(m*i1) = cod m by Th44;
  (m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 by A5,Th44;
  hence m*i1 = m by A4,A1,A6,Lm3,RELAT_1:52;
A7: i2`2 = id (cod m)`2 & cod i2 = cod m by Th46;
A8: dom i2 = cod m by Th46;
  then
A9: cod(i2*m) = cod i2 by Th44;
  (i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m by A8,Th44;
  hence thesis by A3,A7,A9,Lm3,RELAT_1:53;
end;

definition
  let X;
  func fDom X -> Function of MapsT(X),TOL(X) means
  :Def25:
  for m holds it.m = dom m;
  existence
  proof
    deffunc F(Element of MapsT(X)) = dom $1;
    thus ex f being Function of MapsT(X),TOL(X) st for x being Element of
    MapsT(X) holds f.x = F(x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let h1,h2 be Function of MapsT(X),TOL(X) such that
A1: for m holds h1.m = dom m and
A2: for m holds h2.m = dom m;
    now
      let m;
      thus h1.m = dom m by A1
        .= h2.m by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func fCod X -> Function of MapsT(X),TOL(X) means
  :Def26:
  for m holds it.m = cod m;
  existence
  proof
    deffunc F(Element of MapsT(X)) = cod $1;
    thus ex f being Function of MapsT(X),TOL(X) st for x being Element of
    MapsT(X) holds f.x = F(x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let h1,h2 be Function of MapsT(X),TOL(X) such that
A3: for m holds h1.m = cod m and
A4: for m holds h2.m = cod m;
    now
      let m;
      thus h1.m = cod m by A3
        .= h2.m by A4;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func fComp X -> PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) means
  :Def27:
  (
for m2,m1 holds [m2,m1] in dom it iff dom m2 = cod m1) & for m2,m1 st dom m2 =
  cod m1 holds it.[m2,m1] = m2*m1;
  existence
  proof
    defpred P[set,set,set] means for m2,m1 st m2=$1 & m1=$2 holds dom m2 = cod
    m1 & $3 = m2*m1;
A5: for x,y,z1,z2 being set st x in MapsT(X) & y in MapsT(X) & P[x,y,z1]
    & P[x,y,z2] holds z1 = z2
    proof
      let x,y,z1,z2 be set;
      assume x in MapsT(X) & y in MapsT(X);
      then reconsider m2 = x, m1 = y as Element of MapsT(X);
      assume that
A6:   P[x,y,z1] and
A7:   P[x,y,z2];
      z1 = m2*m1 by A6;
      hence thesis by A7;
    end;
A8: for x,y,z being set st x in MapsT(X) & y in MapsT(X) & P[x,y,z] holds
    z in MapsT(X)
    proof
      let x,y,z be set;
      assume x in MapsT(X) & y in MapsT(X);
      then reconsider m2 = x, m1 = y as Element of MapsT(X);
      assume P[x,y,z];
      then z = m2*m1;
      hence thesis;
    end;
    consider h being PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) such that
A9: for x,y holds [x,y] in dom h iff x in MapsT(X) & y in MapsT(X) &
    ex z st P[x,y,z] and
A10: for x,y st [x,y] in dom h holds P[x,y,h.(x,y)] from BINOP_1:sch 5
    (A8, A5);
    take h;
    thus
A11: for m2,m1 holds [m2,m1] in dom h iff dom m2 = cod m1
    proof
      let m2,m1;
      thus [m2,m1] in dom h implies dom m2 = cod m1
      proof
        assume [m2,m1] in dom h;
        then ex z being set st P[m2,m1,z] by A9;
        hence thesis;
      end;
      assume dom m2 = cod m1;
      then P[m2,m1,m2*m1];
      hence thesis by A9;
    end;
    let m2,m1;
    assume dom m2 = cod m1;
    then [m2,m1] in dom h by A11;
    then P[m2,m1,h.(m2,m1)] by A10;
    hence thesis;
  end;
  uniqueness
  proof
    let h1,h2 be PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) such that
A12: for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A13: for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A14: for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A15: for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
A16: dom h1 = dom h2
    proof
      let x,y be set;
      thus [x,y] in dom h1 implies [x,y] in dom h2
      proof
        assume
A17:    [x,y] in dom h1;
        then reconsider m2 = x, m1 = y as Element of MapsT(X) by ZFMISC_1:87;
        dom m2 = cod m1 by A12,A17;
        hence thesis by A14;
      end;
      assume
A18:  [x,y] in dom h2;
      then reconsider m2 = x, m1 = y as Element of MapsT(X) by ZFMISC_1:87;
      dom m2 = cod m1 by A14,A18;
      hence thesis by A12;
    end;
    now
      let m be Element of [:MapsT(X),MapsT(X):] such that
A19:  m in dom h1;
      consider m2,m1 be Element of MapsT(X) such that
A20:  m = [m2,m1] by DOMAIN_1:1;
A21:  dom m2 = cod m1 by A12,A19,A20;
      then h1.[m2,m1] = m2*m1 by A13;
      hence h1.m = h2.m by A15,A20,A21;
    end;
    hence thesis by A16,PARTFUN1:5;
  end;
end;

definition
 canceled;
  let X;
  func TolCat(X) -> non empty non void strict CatStr equals
  CatStr(# TOL(X),MapsT(X),fDom X,fCod X,fComp X#);
  coherence;
end;

registration
  let X;
  cluster TolCat(X) -> Category-like transitive associative reflexive;
  coherence
   proof set C = TolCat X;
    set M = MapsT(X), d = fDom X, c = fCod X, p = fComp X;
thus P1:  C is Category-like
  proof
      let ff,gg be Morphism of C;
      reconsider f=ff, g=gg as Element of M;
      d.g = dom g & c.f = cod f by Def25,Def26;
      hence thesis by Def27;
   end;
thus P2: C is transitive
   proof
      let ff,gg be Morphism of C such that
A1:   dom gg=cod ff;
      [gg,ff] in dom the Comp of C by A1,P1,CAT_1:def 6;
      then
U:    (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
      reconsider f=ff, g=gg as Element of M;
A2:   d.g = dom g & c.f = cod f by Def25,Def26;
      then
A3:   p.[g,f] = g*f by A1,Def27;
A4:   d.f = dom f & c.g = cod g by Def25,Def26;
      dom(g*f) = dom f & cod(g*f) = cod g by A1,A2,Th44;
      hence thesis by A3,A4,Def25,Def26,U;
    end;
thus  C is associative
   proof
      let ff,gg,hh be Morphism of C such that
A5:   dom hh = cod gg and
A6:   dom gg = cod ff;
      reconsider f=ff, g=gg, h=hh as Element of M;
A7:   dom h = d.h & cod g = c.g by Def25,Def26;
      then
A8:   dom(h*g) = dom g by A5,Th44;
A9:   dom g = d.g & cod f = c.f by Def25,Def26;
      then
A10:  cod(g*f) = dom h by A5,A6,A7,Th44;
       [hh,gg] in dom the Comp of C by A5,P1,CAT_1:def 6;
       then
X2:    hh(*)gg = (the Comp of C).(hh,gg) by CAT_1:def 1;
       [gg,ff] in dom the Comp of C by A6,P1,CAT_1:def 6;
       then
X1:    gg(*)ff = (the Comp of C).(gg,ff) by CAT_1:def 1;
       dom(hh(*)gg) = dom gg by P2,CAT_1:def 7,A5;
       then
X3:     [hh(*)gg,ff] in dom the Comp of C by P1,CAT_1:def 6,A6;
       cod(gg(*)ff) = cod gg by P2,CAT_1:def 7,A6;
       then [hh,gg(*)ff] in dom the Comp of C by P1,CAT_1:def 6,A5;
      hence hh(*)(gg(*)ff)
         = (the Comp of C).(hh,(the Comp of C).(gg,ff)) by X1,CAT_1:def 1
        .= p.[h,g*f] by A6,A9,Def27
        .= h*(g*f) by A10,Def27
        .= (h*g)*f by A5,A6,A7,A9,Th45
        .= p.[h*g,f] by A6,A9,A8,Def27
        .= (the Comp of C).((the Comp of C).(hh,gg),ff) by A5,A7,Def27
        .= hh(*)gg(*)ff by X2,X3,CAT_1:def 1;
    end;
    let a be Object of C;
     reconsider aa = a as Element of TOL X;
     reconsider ii = id$ aa as Morphism of C;
A12: cod ii = cod id$ aa by Def26 .= aa by Th46;
     dom ii = dom id$ aa by Def25 .= aa by Th46;
     then id$ aa in Hom(a,a) by A12;
    hence Hom(a,a)<>{};
   end;
end;

LmX:
  for a being Element of TolCat X, aa being Element of TOL X st a = aa
  for i being Morphism of a,a st i = id$ aa
  for b being Element of TolCat X holds
   (Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
   (Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
  proof let a be Element of TolCat X, aa be Element of TOL X such that
Z1: a = aa;
   let i be Morphism of a,a such that
Z2: i = id$ aa;
  let b be Element of TolCat X;
  thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
   proof assume
Z3:  Hom(a,b)<>{};
    let g be Morphism of a,b;
     reconsider gg = g as Element of MapsT X;
     Hom(a,a)<>{};
     then
A1:  cod i = a by CAT_1:5 .= dom g by Z3,CAT_1:5;
A3:  dom gg = dom g by Def25 .= aa by Z1,Z3,CAT_1:5;
     then
A2:  cod id$ aa = dom gg by Th46;
     [g,i] in dom the Comp of TolCat X by A1,CAT_1:def 6;
    hence g(*)i = (the Comp of TolCat X).(g,i) by CAT_1:def 1
       .= gg*id$ aa by A2,Z2,Def27
       .= g by A3,Th47;
   end;
   thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
   proof assume
Z3:  Hom(b,a)<>{};
    let g be Morphism of b,a;
     reconsider gg = g as Element of MapsT X;
     Hom(a,a)<>{};
     then
A1:  dom i = a by CAT_1:5 .= cod g by Z3,CAT_1:5;
A3:  cod gg = cod g by Def26 .= aa by Z1,Z3,CAT_1:5;
     then
A2:  dom id$ aa = cod gg by Th46;
     [i,g] in dom the Comp of TolCat X by A1,CAT_1:def 6;
    hence i(*)g = (the Comp of TolCat X).(i,g) by CAT_1:def 1
       .= (id$ aa)*gg by Z2,A2,Def27
       .= g by A3,Th47;
   end;
  end;

registration
  let X;
  cluster TolCat(X) -> with_identities;
  coherence
  proof let a being Element of TolCat X;
    reconsider aa = a as Element of TOL X;
    reconsider ii = id$ aa as Morphism of TolCat X;
A12: cod ii = cod id$ aa by Def26 .= aa by Th46;
     dom ii = dom id$ aa by Def25 .= aa by Th46;
    then ii in Hom(a,a) by A12;
    then reconsider ii as Morphism of a,a by CAT_1:def 5;
   take ii;
   thus thesis by LmX;
  end;
end;