:: COH_SP semantic presentation

begin


definition
let IT be set ;
attrIT is binary_complete  means :Def1: :: COH_SP:def 1
 for A being set st A c= IT & ( for a, b being set st a in A & b in A holds
a \/ b in IT ) holds
union A in IT;
end;

:: deftheorem Def1 defines binary_complete COH_SP:def_1_:_
 for IT being set holds
( IT is binary_complete iff for A being set st A c= IT & ( for a, b being set st a in A & b in A holds
a \/ b in IT ) holds
union A in IT );

registration
cluster non empty subset-closed binary_complete for set ;
existence
 ex b1 being set st
( b1 is subset-closed & b1 is binary_complete & not b1 is empty )
proof
take X = {{}}; ::_thesis: ( X is subset-closed & X is binary_complete & not X is empty )
thus  for a, b being set st a in X & b c= a holds
b in X :: according to CLASSES1:def_1 ::_thesis: ( X is binary_complete & not X is empty )
proof
let a, b be set ; ::_thesis: ( a in X & b c= a implies b in X )
assume that
A1: a in X and
A2: b c= a ; ::_thesis: b in X
 a = {} by A1, TARSKI:def_1;
hence  b in X by A1, A2; ::_thesis: verum
end;
thus  for A being set st A c= X & ( for a, b being set st a in A & b in A holds
a \/ b in X ) holds
union A in X :: according to COH_SP:def_1 ::_thesis: not X is empty
proof
let A be set ; ::_thesis: ( A c= X & ( for a, b being set st a in A & b in A holds
a \/ b in X ) implies union A in X )
assume that
A3: A c= X and
 for a, b being set st a in A & b in A holds
a \/ b in X ; ::_thesis: union A in X
now__::_thesis:_union_A_in_X
percases ( A = {} or A = {{}} ) by A3, ZFMISC_1:33;
suppose A = {} ; ::_thesis: union A in X
hence  union A in X by TARSKI:def_1, ZFMISC_1:2; ::_thesis: verum
end;
suppose A = {{}} ; ::_thesis: union A in X
then  union A = {} by ZFMISC_1:25;
hence  union A in X by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  union A in X ; ::_thesis: verum
end;
thus  not X is empty ; ::_thesis: verum
end;
end;

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


theorem :: COH_SP:1
for C being Coherence_Space holds {} in C
proof
let C be Coherence_Space; ::_thesis: {} in C
 ( {} c= C & ( for a, b being set st a in {} & b in {} holds
a \/ b in C ) ) by XBOOLE_1:2;
hence  {} in C by Def1, ZFMISC_1:2; ::_thesis: verum
end;

theorem Th2: :: COH_SP:2
for X being set holds bool X is Coherence_Space
proof
let X be set ; ::_thesis: bool X is Coherence_Space
A1: for A being set st A c= bool X & ( for a, b being set st a in A & b in A holds
a \/ b in bool X ) holds
union A in bool X
proof
let A be set ; ::_thesis: ( A c= bool X & ( for a, b being set st a in A & b in A holds
a \/ b in bool X ) implies union A in bool X )
assume that
A2: A c= bool X and
 for a, b being set st a in A & b in A holds
a \/ b in bool X ; ::_thesis: union A in bool X
 for a being set st a in A holds
a c= X by A2;
then  union A c= X by ZFMISC_1:76;
hence  union A in bool X ; ::_thesis: verum
end;
 for a, b being set st a in bool X & b c= a holds
b in bool X
proof
let a, b be set ; ::_thesis: ( a in bool X & b c= a implies b in bool X )
assume  ( a in bool X & b c= a ) ; ::_thesis: b in bool X
then  b c= X by XBOOLE_1:1;
hence  b in bool X ; ::_thesis: verum
end;
hence  bool X is Coherence_Space by A1, Def1, CLASSES1:def_1; ::_thesis: verum
end;

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

theorem Th4: :: COH_SP:4
for x being set
for C being Coherence_Space st x in union C holds
{x} in C
proof
let x be set ; ::_thesis: for C being Coherence_Space st x in union C holds
{x} in C
let C be Coherence_Space; ::_thesis: ( x in union C implies {x} in C )
assume  x in union C ; ::_thesis: {x} in C
then consider X being set  such that
A1: x in X and
A2: X in C by TARSKI:def_4;
 {x} c= X by A1, ZFMISC_1:31;
hence  {x} in C by A2, CLASSES1:def_1; ::_thesis: verum
end;

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

:: deftheorem Def2 defines Web COH_SP:def_2_:_
 for C being Coherence_Space
for b2 being Tolerance of (union C) holds
( b2 = Web C iff for x, y being set holds
( [x,y] in b2 iff ex X being set st
( X in C & x in X & y in X ) ) );

theorem Th5: :: COH_SP:5
for C being Coherence_Space
for T being Tolerance of (union C) holds
( T = Web C iff for x, y being set holds
( [x,y] in T iff {x,y} in C ) )
proof
let C be Coherence_Space; ::_thesis: for T being Tolerance of (union C) holds
( T = Web C iff for x, y being set holds
( [x,y] in T iff {x,y} in C ) )
let T be Tolerance of (union C); ::_thesis: ( T = Web C iff for x, y being set holds
( [x,y] in T iff {x,y} in C ) )
thus  ( T = Web C implies for x, y being set holds
( [x,y] in T iff {x,y} in C ) ) ::_thesis: ( ( for x, y being set holds
( [x,y] in T iff {x,y} in C ) ) implies T = Web C )
proof
assume A1: T = Web C ; ::_thesis: for x, y being set holds
( [x,y] in T iff {x,y} in C )
let x, y be set ; ::_thesis: ( [x,y] in T iff {x,y} in C )
thus  ( [x,y] in T implies {x,y} in C ) ::_thesis: ( {x,y} in C implies [x,y] in T )
proof
assume  [x,y] in T ; ::_thesis: {x,y} in C
then consider X being set  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  {x,y} in C by A2, CLASSES1:def_1; ::_thesis: verum
end;
A4: ( x in {x,y} & y in {x,y} ) by TARSKI:def_2;
assume  {x,y} in C ; ::_thesis: [x,y] in T
hence  [x,y] in T by A1, A4, Def2; ::_thesis: verum
end;
assume A5: for x, y being set holds
( [x,y] in T iff {x,y} in C ) ; ::_thesis: T = Web C
 for x, y being set holds
( [x,y] in T iff ex X being set st
( X in C & x in X & y in X ) )
proof
let x, y be set ; ::_thesis: ( [x,y] in T iff ex X being set st
( X in C & x in X & y in X ) )
thus  ( [x,y] in T implies ex X being set st
( X in C & x in X & y in X ) ) ::_thesis: ( ex X being set st
( X in C & x in X & y in X ) implies [x,y] in T )
proof
assume A6: [x,y] in T ; ::_thesis: ex X being set st
( X in C & x in X & y in X )
take  {x,y} ; ::_thesis: ( {x,y} in C & x in {x,y} & y in {x,y} )
thus  ( {x,y} in C & x in {x,y} & y in {x,y} ) by A5, A6, TARSKI:def_2; ::_thesis: verum
end;
given X being set  such that A7: X in C and
A8: ( x in X & y in X ) ; ::_thesis: [x,y] in T
 {x,y} c= X by A8, ZFMISC_1:32;
then  {x,y} in C by A7, CLASSES1:def_1;
hence  [x,y] in T by A5; ::_thesis: verum
end;
hence  T = Web C by Def2; ::_thesis: verum
end;

theorem Th6: :: COH_SP:6
for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
proof
let a be set ; ::_thesis: for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
let C be Coherence_Space; ::_thesis: ( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
defpred S1[ set , set ] means {$1} = $2;
thus  ( a in C implies for x, y being set st x in a & y in a holds
{x,y} in C ) ::_thesis: ( ( for x, y being set st x in a & y in a holds
{x,y} in C ) implies a in C )
proof
assume A1: a in C ; ::_thesis: for x, y being set st x in a & y in a holds
{x,y} in C
let x, y be set ; ::_thesis: ( x in a & y in a implies {x,y} in C )
assume  ( x in a & y in a ) ; ::_thesis: {x,y} in C
then  {x,y} c= a by ZFMISC_1:32;
hence  {x,y} in C by A1, CLASSES1:def_1; ::_thesis: verum
end;
A2: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z ;
consider X being set  such that
A3: for x being set holds
( x in X iff ex y being set st
( y in a & S1[y,x] ) ) from TARSKI:sch_1(A2);
assume A4: for x, y being set st x in a & y in a holds
{x,y} in C ; ::_thesis: a in C
A5: for b, c being set st b in X & c in X holds
b \/ c in C
proof
let b, c be set ; ::_thesis: ( b in X & c in X implies b \/ c in C )
assume that
A6: b in X and
A7: c in X ; ::_thesis: b \/ c in C
consider z being set  such that
A8: z in a and
A9: {z} = c by A3, A7;
consider y being set  such that
A10: y in a and
A11: {y} = b by A3, A6;
 {y,z} in C by A4, A10, A8;
hence  b \/ c in C by A11, A9, ENUMSET1:1; ::_thesis: verum
end;
A12: union X = a
proof
thus  union X c= a :: according to XBOOLE_0:def_10 ::_thesis: a c= union X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in a )
assume  x in union X ; ::_thesis: x in a
then consider Z being set  such that
A13: x in Z and
A14: Z in X by TARSKI:def_4;
 ex y being set st
( y in a & Z = {y} ) by A3, A14;
hence  x in a by A13, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in union X )
assume  x in a ; ::_thesis: x in union X
then A15: {x} in X by A3;
 x in {x} by TARSKI:def_1;
hence  x in union X by A15, TARSKI:def_4; ::_thesis: verum
end;
 X c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in C )
assume  x in X ; ::_thesis: x in C
then consider y being set  such that
A16: y in a and
A17: {y} = x by A3;
 {y,y} in C by A4, A16;
hence  x in C by A17, ENUMSET1:29; ::_thesis: verum
end;
hence  a in C by A5, A12, Def1; ::_thesis: verum
end;

theorem Th7: :: COH_SP:7
for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
proof
let a be set ; ::_thesis: for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
let C be Coherence_Space; ::_thesis: ( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
thus  ( a in C implies for x, y being set st x in a & y in a holds
[x,y] in Web C ) ::_thesis: ( ( for x, y being set st x in a & y in a holds
[x,y] in Web C ) implies a in C )
proof
assume A1: a in C ; ::_thesis: for x, y being set st x in a & y in a holds
[x,y] in Web C
let x, y be set ; ::_thesis: ( x in a & y in a implies [x,y] in Web C )
assume  ( x in a & y in a ) ; ::_thesis: [x,y] in Web C
then  {x,y} in C by A1, Th6;
hence  [x,y] in Web C by Th5; ::_thesis: verum
end;
assume A2: for x, y being set st x in a & y in a holds
[x,y] in Web C ; ::_thesis: a in C
now__::_thesis:_for_x,_y_being_set_st_x_in_a_&_y_in_a_holds_
{x,y}_in_C
let x, y be set ; ::_thesis: ( x in a & y in a implies {x,y} in C )
assume  ( x in a & y in a ) ; ::_thesis: {x,y} in C
then  [x,y] in Web C by A2;
hence  {x,y} in C by Th5; ::_thesis: verum
end;
hence  a in C by Th6; ::_thesis: verum
end;

theorem :: COH_SP:8
for a being set
for C being Coherence_Space st ( for x, y being set st x in a & y in a holds
{x,y} in C ) holds
a c= union C
proof
let a be set ; ::_thesis: for C being Coherence_Space st ( for x, y being set st x in a & y in a holds
{x,y} in C ) holds
a c= union C
let C be Coherence_Space; ::_thesis: ( ( for x, y being set st x in a & y in a holds
{x,y} in C ) implies a c= union C )
assume A1: for x, y being set st x in a & y in a holds
{x,y} in C ; ::_thesis: a c= union C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in union C )
assume  x in a ; ::_thesis: x in union C
then  {x,x} in C by A1;
then A2: {x} in C by ENUMSET1:29;
 x in {x} by TARSKI:def_1;
hence  x in union C by A2, TARSKI:def_4; ::_thesis: verum
end;

theorem :: COH_SP:9
for C, D being Coherence_Space st Web C = Web D holds
C = D
proof
let C, D be Coherence_Space; ::_thesis: ( Web C = Web D implies C = D )
assume A1: Web C = Web D ; ::_thesis: C = D
thus  C c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in D )
assume  x in C ; ::_thesis: x in D
then  for z, y being set st z in x & y in x holds
[z,y] in Web D by A1, Th7;
hence  x in D by Th7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in C )
assume  x in D ; ::_thesis: x in C
then  for z, y being set st z in x & y in x holds
[z,y] in Web C by A1, Th7;
hence  x in C by Th7; ::_thesis: verum
end;

theorem :: COH_SP:10
for C being Coherence_Space st union C in C holds
C = bool (union C)
proof
let C be Coherence_Space; ::_thesis: ( union C in C implies C = bool (union C) )
assume A1: union C in C ; ::_thesis: C = bool (union C)
thus  C c= bool (union C) by ZFMISC_1:82; :: according to XBOOLE_0:def_10 ::_thesis: bool (union C) c= C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool (union C) or x in C )
assume  x in bool (union C) ; ::_thesis: x in C
hence  x in C by A1, CLASSES1:def_1; ::_thesis: verum
end;

theorem :: COH_SP:11
for C being Coherence_Space st C = bool (union C) holds
Web C = Total (union C)
proof
let C be Coherence_Space; ::_thesis: ( C = bool (union C) implies Web C = Total (union C) )
reconsider t = Total (union C) as Tolerance of (union C) ;
assume A1: C = bool (union C) ; ::_thesis: Web C = Total (union C)
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_t_implies_{x,y}_in_C_)_&_(_{x,y}_in_C_implies_[x,y]_in_t_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in t implies {x,y} in C ) & ( {x,y} in C implies [x,y] in t ) )
thus  ( [x,y] in t implies {x,y} in C ) ::_thesis: ( {x,y} in C implies [x,y] in t )
proof
assume  [x,y] in t ; ::_thesis: {x,y} in C
then A2: ( x in union C & y in union C ) by ZFMISC_1:87;
 {x,y} c= union C
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in union C )
assume  z in {x,y} ; ::_thesis: z in union C
hence  z in union C by A2, TARSKI:def_2; ::_thesis: verum
end;
hence  {x,y} in C by A1; ::_thesis: verum
end;
assume  {x,y} in C ; ::_thesis: [x,y] in t
then  ( x in union C & y in union C ) by A1, ZFMISC_1:32;
hence  [x,y] in t by TOLER_1:2; ::_thesis: verum
end;
hence  Web C = Total (union C) by Th5; ::_thesis: verum
end;

definition
let X be set ;
let E be Tolerance of X;
func CohSp E ->  Coherence_Space means :Def3: :: COH_SP:def 3
 for a being set holds
( a in it iff for x, y being set st x in a & y in a holds
[x,y] in E );
existence
 ex b1 being Coherence_Space st
for a being set holds
( a in b1 iff for x, y being set st x in a & y in a holds
[x,y] in E )
proof
defpred S1[ set ] means  for x, y being set st x in $1 & y in $1 holds
[x,y] in E;
consider Z being set  such that
A1: for x being set holds
( x in Z iff ( x in bool X & S1[x] ) ) from XBOOLE_0:sch_1();
A2: for A being set st A c= Z & ( for a, b being set st a in A & b in A holds
a \/ b in Z ) holds
union A in Z
proof
let A be set ; ::_thesis: ( A c= Z & ( for a, b being set st a in A & b in A holds
a \/ b in Z ) implies union A in Z )
assume that
A3: A c= Z and
A4: for a, b being set st a in A & b in A holds
a \/ b in Z ; ::_thesis: union A in Z
A5: now__::_thesis:_for_x,_y_being_set_st_x_in_union_A_&_y_in_union_A_holds_
[x,y]_in_E
let x, y be set ; ::_thesis: ( x in union A & y in union A implies [x,y] in E )
assume that
A6: x in union A and
A7: y in union A ; ::_thesis: [x,y] in E
consider Y1 being set  such that
A8: y in Y1 and
A9: Y1 in A by A7, TARSKI:def_4;
consider X1 being 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; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_c=_X
let a be set ; ::_thesis: ( a in A implies a c= X )
assume  a in A ; ::_thesis: a c= X
then  a in bool X by A1, A3;
hence  a c= X ; ::_thesis: verum
end;
then  union A c= X by ZFMISC_1:76;
hence  union A in Z by A1, A5; ::_thesis: verum
end;
A14: for a, b being set st a in Z & b c= a holds
b in Z
proof
let a, b be set ; ::_thesis: ( a in Z & b c= a implies b in Z )
assume that
A15: a in Z and
A16: b c= a ; ::_thesis: b in Z
 a in bool X by A1, A15;
then A17: b c= X by A16, XBOOLE_1:1;
 for x, y being set st x in b & y in b holds
[x,y] in E by A1, A15, A16;
hence  b in Z by A1, A17; ::_thesis: verum
end;
 ( S1[ {} ] & {} c= X ) by XBOOLE_1:2;
then reconsider Z = Z as Coherence_Space by A1, A14, A2, Def1, CLASSES1:def_1;
take  Z ; ::_thesis: for a being set holds
( a in Z iff for x, y being set st x in a & y in a holds
[x,y] in E )
let a be set ; ::_thesis: ( a in Z iff for x, y being set st x in a & y in a holds
[x,y] in E )
thus  ( a in Z implies for x, y being set st x in a & y in a holds
[x,y] in E ) by A1; ::_thesis: ( ( for x, y being set st x in a & y in a holds
[x,y] in E ) implies a in Z )
assume A18: for x, y being set st x in a & y in a holds
[x,y] in E ; ::_thesis: a in Z
then  a c= X by TOLER_1:18, TOLER_1:def_1;
hence  a in Z by A1, A18; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Coherence_Space st ( for a being set holds
( a in b1 iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) & ( for a being set holds
( a in b2 iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) holds
b1 = b2
proof
let C, D be Coherence_Space; ::_thesis: ( ( for a being set holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) & ( for a being set holds
( a in D iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) implies C = D )
assume that
A19: for a being set holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in E ) and
A20: for a being set holds
( a in D iff for x, y being set st x in a & y in a holds
[x,y] in E ) ; ::_thesis: C = D
thus  C c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in D )
assume  x in C ; ::_thesis: x in D
then  for z, y being set st z in x & y in x holds
[z,y] in E by A19;
hence  x in D by A20; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in C )
assume  x in D ; ::_thesis: x in C
then  for z, y being set st z in x & y in x holds
[z,y] in E by A20;
hence  x in C by A19; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines CohSp COH_SP:def_3_:_
 for X being set
for E being Tolerance of X
for b3 being Coherence_Space holds
( b3 = CohSp E iff for a being set holds
( a in b3 iff for x, y being set st x in a & y in a holds
[x,y] in E ) );

theorem :: COH_SP:12
for X being set
for E being Tolerance of X holds Web (CohSp E) = E
proof
let X be set ; ::_thesis: for E being Tolerance of X holds Web (CohSp E) = E
let E be Tolerance of X; ::_thesis: Web (CohSp E) = E
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_Web_(CohSp_E)_implies_[x,y]_in_E_)_&_(_[x,y]_in_E_implies_[x,y]_in_Web_(CohSp_E)_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in Web (CohSp E) implies [x,y] in E ) & ( [x,y] in E implies [x,y] in Web (CohSp E) ) )
thus  ( [x,y] in Web (CohSp E) implies [x,y] in E ) ::_thesis: ( [x,y] in E implies [x,y] in Web (CohSp E) )
proof
assume  [x,y] in Web (CohSp E) ; ::_thesis: [x,y] in E
then A1: {x,y} in CohSp E by Th5;
 ( x in {x,y} & y in {x,y} ) by TARSKI:def_2;
hence  [x,y] in E by A1, Def3; ::_thesis: verum
end;
assume A2: [x,y] in E ; ::_thesis: [x,y] in Web (CohSp E)
then A3: ( x in X & y in X ) by ZFMISC_1:87;
 for u, v being set st u in {x,y} & v in {x,y} holds
[u,v] in E
proof
let u, v be set ; ::_thesis: ( u in {x,y} & v in {x,y} implies [u,v] in E )
assume that
A4: u in {x,y} and
A5: v in {x,y} ; ::_thesis: [u,v] in E
A6: ( v = x or v = y ) by A5, TARSKI:def_2;
 ( u = x or u = y ) by A4, TARSKI:def_2;
hence  [u,v] in E by A2, A3, A6, EQREL_1:6, TOLER_1:7; ::_thesis: verum
end;
then  {x,y} in CohSp E by Def3;
hence  [x,y] in Web (CohSp E) by Th5; ::_thesis: verum
end;
hence  Web (CohSp E) = E by RELAT_1:def_2; ::_thesis: verum
end;

theorem :: COH_SP:13
for C being Coherence_Space holds CohSp (Web C) = C
proof
let C be Coherence_Space; ::_thesis: CohSp (Web C) = C
thus  CohSp (Web C) c= C :: according to XBOOLE_0:def_10 ::_thesis: C c= CohSp (Web C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in CohSp (Web C) or x in C )
assume  x in CohSp (Web C) ; ::_thesis: x in C
then  for y, z being set st y in x & z in x holds
[y,z] in Web C by Def3;
hence  x in C by Th7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in CohSp (Web C) )
assume  x in C ; ::_thesis: x in CohSp (Web C)
then  for y, z being set st y in x & z in x holds
[y,z] in Web C by Th7;
hence  x in CohSp (Web C) by Def3; ::_thesis: verum
end;

theorem Th14: :: COH_SP:14
for X, a being set
for E being Tolerance of X holds
( a in CohSp E iff a is TolSet of E )
proof
let X, a be set ; ::_thesis: for E being Tolerance of X holds
( a in CohSp E iff a is TolSet of E )
let E be Tolerance of X; ::_thesis: ( a in CohSp E iff a is TolSet of E )
thus  ( a in CohSp E implies a is TolSet of E ) ::_thesis: ( a is TolSet of E implies a in CohSp E )
proof
assume  a in CohSp E ; ::_thesis: a is TolSet of E
then  for x, y being set st x in a & y in a holds
[x,y] in E by Def3;
hence  a is TolSet of E by TOLER_1:def_1; ::_thesis: verum
end;
assume  a is TolSet of E ; ::_thesis: a in CohSp E
then  for x, y being set st x in a & y in a holds
[x,y] in E by TOLER_1:def_1;
hence  a in CohSp E by Def3; ::_thesis: verum
end;

theorem :: COH_SP:15
for X being set
for E being Tolerance of X holds CohSp E = TolSets E
proof
let X be set ; ::_thesis: for E being Tolerance of X holds CohSp E = TolSets E
let E be Tolerance of X; ::_thesis: CohSp E = TolSets E
thus  CohSp E c= TolSets E :: according to XBOOLE_0:def_10 ::_thesis: TolSets E c= CohSp E
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in CohSp E or x in TolSets E )
assume  x in CohSp E ; ::_thesis: x in TolSets E
then  x is TolSet of E by Th14;
hence  x in TolSets E by TOLER_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TolSets E or x in CohSp E )
assume  x in TolSets E ; ::_thesis: x in CohSp E
then  x is TolSet of E by TOLER_1:def_3;
hence  x in CohSp E by Th14; ::_thesis: verum
end;

begin

definition
let X be set ;
func CSp X ->  set  equals :: COH_SP:def 4
 {  x where x is Subset-Family of X : x is Coherence_Space  }  ;
coherence
  {  x where x is Subset-Family of X : x is Coherence_Space  }  is set ;
end;

:: deftheorem  defines CSp COH_SP:def_4_:_
 for X being set holds CSp X =  {  x where x is Subset-Family of X : x is Coherence_Space  }  ;

registration
let X be set ;
cluster CSp X ->  non empty ;
coherence
 not CSp X is empty
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  {  x where x is Subset-Family of X : x is Coherence_Space  }  ;
hence  not CSp X is empty ; ::_thesis: verum
end;
end;

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


theorem Th16: :: COH_SP:16
for X, x, y being set
for C being Element of CSp X st {x,y} in C holds
( x in union C & y in union C )
proof
let X, x, y be set ; ::_thesis: for C being Element of CSp X st {x,y} in C holds
( x in union C & y in union C )
let C be Element of CSp X; ::_thesis: ( {x,y} in C implies ( x in union C & y in union C ) )
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 ; ::_thesis: ( x in union C & y in union C )
hence  ( x in union C & y in union C ) by A1, A2, TARSKI:def_4; ::_thesis: verum
end;

definition
let X be set ;
func FuncsC X ->  set  equals :: COH_SP:def 5
 union  {  (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum  }  ;
coherence
 union  {  (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum  }  is set ;
end;

:: deftheorem  defines FuncsC COH_SP:def_5_:_
 for X being set holds FuncsC X = union  {  (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum  }  ;

registration
let X be set ;
cluster FuncsC X ->  functional non empty ;
coherence
 ( not FuncsC X is empty & FuncsC X is functional )
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 = A as Element of CSp X ;
set F =  {  (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum  }  ;
 ( id (union A) in Funcs ((union A),(union A)) & Funcs ((union A),(union A)) in  {  (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum  }  ) by FUNCT_2:9;
then reconsider UF = union  {  (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum  }  as non empty set by TARSKI:def_4;
now__::_thesis:_for_f_being_set_st_f_in_UF_holds_
f_is_Function
let f be set ; ::_thesis: ( f in UF implies f is Function )
assume  f in UF ; ::_thesis: f is Function
then consider C being set  such that
A1: f in C and
A2: C in  {  (Funcs ((union T),(union TT))) where T, TT is Element of CSp X : verum  }  by TARSKI:def_4;
 ex A, B being Element of CSp X st C = Funcs ((union A),(union B)) by A2;
hence  f is Function by A1; ::_thesis: verum
end;
hence  ( not FuncsC X is empty & FuncsC X is functional ) by FUNCT_1:def_13; ::_thesis: verum
end;
end;

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

definition
let X be set ;
func MapsC X ->  set  equals :: COH_SP:def 6
 {  [[C,CC],f] where C, 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 being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) )  }  ;
coherence
  {  [[C,CC],f] where C, 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 being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) )  }  is set ;
end;

:: deftheorem  defines MapsC COH_SP:def_6_:_
 for X being set holds MapsC X =  {  [[C,CC],f] where C, 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 being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) )  }  ;

registration
let X be set ;
cluster MapsC X ->  non empty ;
coherence
 not MapsC X is empty
proof
set FV =  {  [[T,TT],f] where T, 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 being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) )  }  ;
now__::_thesis:_ex_m_being_set_st_m_in__{__[[T,TT],f]_where_T,_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_being_set_st_{x,y}_in_T_holds_
{(f_._x),(f_._y)}_in_TT_)_)__}_
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 = A as Element of CSp X ;
set f = id (union A);
take m = [[A,A],(id (union A))]; ::_thesis: m in  {  [[T,TT],f] where T, 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 being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) )  }
A1: ( union A = {} implies union A = {} ) ;
reconsider f = id (union A) as Element of FuncsC X by Th17;
now__::_thesis:_for_x,_y_being_set_st_{x,y}_in_A_holds_
{(f_._x),(f_._y)}_in_A
let x, y be set ; ::_thesis: ( {x,y} in A implies {(f . x),(f . y)} in A )
assume A2: {x,y} in A ; ::_thesis: {(f . x),(f . 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; ::_thesis: verum
end;
hence  m in  {  [[T,TT],f] where T, 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 being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) )  }  by A1; ::_thesis: verum
end;
hence  not MapsC X is empty ; ::_thesis: verum
end;
end;


theorem Th18: :: COH_SP:18
for X being set
for l being Element of MapsC X ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) )
proof
let X be set ; ::_thesis: for l being Element of MapsC X ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) )
let l be Element of MapsC X; ::_thesis: ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) )
 l in  {  [[C1,C2],g] where C1, C2 is Element of CSp X, g is Element of FuncsC X : ( ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) )  }  ;
then  ex C1, C2 being Element of CSp X ex g being Element of FuncsC X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) ) ;
hence  ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) ) ; ::_thesis: verum
end;

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

registration
let X be set ;
let l be Element of MapsC X;
clusterl `2  ->  Relation-like Function-like ;
coherence
 ( l `2 is Function-like & l `2 is Relation-like )
proof
consider g being Element of FuncsC X, C1, C2 being 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 being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) ) by Th18;
 [[C1,C2],g] `2 = g ;
hence  ( l `2 is Function-like & l `2 is Relation-like ) by W; ::_thesis: verum
end;
end;

definition
let X be set ;
let l be Element of MapsC X;
func dom l ->  Element of CSp X equals :: COH_SP:def 7
(l `1) `1 ;
coherence
 (l `1) `1 is Element of CSp X
proof
consider g being Element of FuncsC X, C1, C2 being Element of CSp X 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 being set 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  (l `1) `1 is Element of CSp X by A1; ::_thesis: verum
end;
func cod l ->  Element of CSp X equals :: COH_SP:def 8
(l `1) `2 ;
coherence
 (l `1) `2 is Element of CSp X
proof
consider g being Element of FuncsC X, C1, C2 being Element of CSp X 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 being set 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  (l `1) `2 is Element of CSp X by A2; ::_thesis: verum
end;
end;

:: deftheorem  defines dom COH_SP:def_7_:_
 for X being set
for l being Element of MapsC X holds dom l = (l `1) `1 ;

:: deftheorem  defines cod COH_SP:def_8_:_
 for X being set
for l being Element of MapsC X holds cod l = (l `1) `2 ;

theorem Th20: :: COH_SP:20
for X being set
for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2)]
proof
let X be set ; ::_thesis: for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2)]
let l be Element of MapsC X; ::_thesis: l = [[(dom l),(cod l)],(l `2)]
consider g being Element of FuncsC X, C1, C2 being Element of CSp X 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 being set 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  l = [[(dom l),(cod l)],(l `2)] by A1, MCART_1:8; ::_thesis: verum
end;

Lm1:  for X being set
for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds
l = l1
proof
let X be set ; ::_thesis: for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds
l = l1
let l, l1 be Element of MapsC X; ::_thesis: ( l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 implies l = l1 )
 l = [[(dom l),(cod l)],(l `2)] by Th20;
hence  ( l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 implies l = l1 ) by Th20; ::_thesis: verum
end;

definition
let X be set ;
let C be Element of CSp X;
func id$ C ->  Element of MapsC X equals :: COH_SP:def 9
[[C,C],(id (union C))];
coherence
 [[C,C],(id (union C))] is Element of MapsC X
proof
set f = id (union C);
now__::_thesis:_for_x,_y_being_set_st_{x,y}_in_C_holds_
{((id_(union_C))_._x),((id_(union_C))_._y)}_in_C
let x, y be set ; ::_thesis: ( {x,y} in C implies {((id (union C)) . x),((id (union C)) . y)} in C )
assume A1: {x,y} in C ; ::_thesis: {((id (union C)) . x),((id (union C)) . 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  {((id (union C)) . x),((id (union C)) . y)} in C by A1, A2, FUNCT_1:18; ::_thesis: verum
end;
hence  [[C,C],(id (union C))] is Element of MapsC X by Th19; ::_thesis: verum
end;
end;

:: deftheorem  defines id$ COH_SP:def_9_:_
 for X being set
for C being Element of CSp X holds id$ C = [[C,C],(id (union C))];

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 ; ::_thesis: ( [[x1,x2],x3] = [[y1,y2],y3] implies ( x1 = y1 & x2 = y2 ) )
assume  [[x1,x2],x3] = [[y1,y2],y3] ; ::_thesis: ( x1 = y1 & x2 = y2 )
then  [x1,x2] = [y1,y2] by XTUPLE_0:1;
hence  ( x1 = y1 & x2 = y2 ) by XTUPLE_0:1; ::_thesis: verum
end;

theorem Th21: :: COH_SP:21
for X being set
for l being Element of MapsC X holds
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )
proof
let X be set ; ::_thesis: for l being Element of MapsC X holds
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )
let l be Element of MapsC X; ::_thesis: ( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )
consider g being Element of FuncsC X, C1, C2 being Element of CSp X 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 being set 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; ::_thesis: for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l
let x, y be set ; ::_thesis: ( {x,y} in dom l implies {((l `2) . x),((l `2) . y)} in cod l )
assume  {x,y} in dom l ; ::_thesis: {((l `2) . x),((l `2) . y)} in cod l
hence  {((l `2) . x),((l `2) . y)} in cod l by A3, A6, A5; ::_thesis: verum
end;

definition
let X be set ;
let l1, l2 be Element of MapsC X;
assume A1: cod l1 = dom l2 ;
funcl2 * l1 ->  Element of MapsC X equals :Def10: :: COH_SP:def 10
[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];
coherence
 [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X
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__::_thesis:_for_x,_y_being_set_st_{x,y}_in_dom_l1_holds_
{(((l2_`2)_*_(l1_`2))_._x),(((l2_`2)_*_(l1_`2))_._y)}_in_cod_l2
let x, y be set ; ::_thesis: ( {x,y} in dom l1 implies {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2 )
assume A6: {x,y} in dom l1 ; ::_thesis: {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2
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; ::_thesis: verum
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  [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X by A1, A3, A2, A5, Th19; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines * COH_SP:def_10_:_
 for X being set
for l1, l2 being Element of MapsC X st cod l1 = dom l2 holds
l2 * l1 = [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];

theorem Th22: :: COH_SP:22
for X being set
for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
proof
let X be set ; ::_thesis: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
let l2, l1 be Element of MapsC X; ::_thesis: ( dom l2 = cod l1 implies ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) )
assume  dom l2 = cod l1 ; ::_thesis: ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
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  ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) by Lm2, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th23: :: COH_SP:23
for X being set
for l2, l1, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds
l3 * (l2 * l1) = (l3 * l2) * l1
proof
let X be set ; ::_thesis: for l2, l1, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds
l3 * (l2 * l1) = (l3 * l2) * l1
let l2, l1, l3 be Element of MapsC X; ::_thesis: ( dom l2 = cod l1 & dom l3 = cod l2 implies l3 * (l2 * l1) = (l3 * l2) * l1 )
assume that
A1: dom l2 = cod l1 and
A2: dom l3 = cod l2 ; ::_thesis: l3 * (l2 * l1) = (l3 * l2) * l1
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  l3 * (l2 * l1) = (l3 * l2) * l1 by A4, A7, A9, A6, A8, Lm1, RELAT_1:36; ::_thesis: verum
end;

theorem Th24: :: COH_SP:24
for X being set
for C being Element of CSp X holds
( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
proof
let X be set ; ::_thesis: for C being Element of CSp X holds
( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
let C be Element of CSp X; ::_thesis: ( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
 [[(dom (id$ C)),(cod (id$ C))],((id$ C) `2)] = [[C,C],(id (union C))] by Th20;
hence  ( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C ) by Lm2, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th25: :: COH_SP:25
for X being set
for l being Element of MapsC X holds
( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
proof
let X be set ; ::_thesis: for l being Element of MapsC X holds
( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
let l be Element of MapsC X; ::_thesis: ( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
set i1 = id$ (dom l);
set i2 = id$ (cod l);
A1: ( (id$ (dom l)) `2 = id (union (dom l)) & dom (id$ (dom l)) = 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 (id$ (dom l)) = dom l by Th24;
then A6: cod (l * (id$ (dom l))) = cod l by Th22;
 ( (l * (id$ (dom l))) `2 = (l `2) * ((id$ (dom l)) `2) & dom (l * (id$ (dom l))) = dom (id$ (dom l)) ) by A5, Th22;
hence  l * (id$ (dom l)) = l by A4, A1, A6, Lm1, RELAT_1:52; ::_thesis: (id$ (cod l)) * l = l
A7: ( (id$ (cod l)) `2 = id (union (cod l)) & cod (id$ (cod l)) = cod l ) by Th24;
A8: dom (id$ (cod l)) = cod l by Th24;
then A9: cod ((id$ (cod l)) * l) = cod (id$ (cod l)) by Th22;
 ( ((id$ (cod l)) * l) `2 = ((id$ (cod l)) `2) * (l `2) & dom ((id$ (cod l)) * l) = dom l ) by A8, Th22;
hence  (id$ (cod l)) * l = l by A3, A7, A9, Lm1, RELAT_1:53; ::_thesis: verum
end;

definition
let X be set ;
func CDom X ->  Function of (MapsC X),(CSp X) means :Def11: :: COH_SP:def 11
 for l being Element of MapsC X holds it . l = dom l;
existence
 ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = dom l
proof
deffunc H1( Element of MapsC X) ->  Element of CSp X = dom $1;
thus  ex f being Function of (MapsC X),(CSp X) st
for x being Element of MapsC X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = dom l ) & ( for l being Element of MapsC X holds b2 . l = dom l ) holds
b1 = b2
proof
let h1, h2 be Function of (MapsC X),(CSp X); ::_thesis: ( ( for l being Element of MapsC X holds h1 . l = dom l ) & ( for l being Element of MapsC X holds h2 . l = dom l ) implies h1 = h2 )
assume that
A1: for l being Element of MapsC X holds h1 . l = dom l and
A2: for l being Element of MapsC X holds h2 . l = dom l ; ::_thesis: h1 = h2
now__::_thesis:_for_l_being_Element_of_MapsC_X_holds_h1_._l_=_h2_._l
let l be Element of MapsC X; ::_thesis: h1 . l = h2 . l
thus h1 . l = dom l by A1
.= h2 . l by A2 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func CCod X ->  Function of (MapsC X),(CSp X) means :Def12: :: COH_SP:def 12
 for l being Element of MapsC X holds it . l = cod l;
existence
 ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = cod l
proof
deffunc H1( Element of MapsC X) ->  Element of CSp X = cod $1;
thus  ex f being Function of (MapsC X),(CSp X) st
for x being Element of MapsC X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = cod l ) & ( for l being Element of MapsC X holds b2 . l = cod l ) holds
b1 = b2
proof
let h1, h2 be Function of (MapsC X),(CSp X); ::_thesis: ( ( for l being Element of MapsC X holds h1 . l = cod l ) & ( for l being Element of MapsC X holds h2 . l = cod l ) implies h1 = h2 )
assume that
A3: for l being Element of MapsC X holds h1 . l = cod l and
A4: for l being Element of MapsC X holds h2 . l = cod l ; ::_thesis: h1 = h2
now__::_thesis:_for_l_being_Element_of_MapsC_X_holds_h1_._l_=_h2_._l
let l be Element of MapsC X; ::_thesis: h1 . l = h2 . l
thus h1 . l = cod l by A3
.= h2 . l by A4 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func CComp X ->  PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) means :Def13: :: COH_SP:def 13
( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom it iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
it . [l2,l1] = l2 * l1 ) );
existence
 ex b1 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st
( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) )
proof
defpred S1[ set , set , set ] means  for l2, l1 being Element of MapsC X 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 & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
proof
let x, y, z1, z2 be set ; ::_thesis: ( x in MapsC X & y in MapsC X & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume  ( x in MapsC X & y in MapsC X ) ; ::_thesis: ( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 )
then reconsider l2 = x, l1 = y as Element of MapsC X ;
assume that
A6: S1[x,y,z1] and
A7: S1[x,y,z2] ; ::_thesis: z1 = z2
 z1 = l2 * l1 by A6;
hence  z1 = z2 by A7; ::_thesis: verum
end;
A8: for x, y, z being set st x in MapsC X & y in MapsC X & S1[x,y,z] holds
z in MapsC X
proof
let x, y, z be set ; ::_thesis: ( x in MapsC X & y in MapsC X & S1[x,y,z] implies z in MapsC X )
assume  ( x in MapsC X & y in MapsC X ) ; ::_thesis: ( not S1[x,y,z] or z in MapsC X )
then reconsider l2 = x, l1 = y as Element of MapsC X ;
assume  S1[x,y,z] ; ::_thesis: z in MapsC X
then  z = l2 * l1 ;
hence  z in MapsC X ; ::_thesis: verum
end;
consider h being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) such that
A9: for x, y being set holds
( [x,y] in dom h iff ( x in MapsC X & y in MapsC X & ex z being set st S1[x,y,z] ) ) and
A10: for x, y being set st [x,y] in dom h holds
S1[x,y,h . (x,y)] from BINOP_1:sch_5(A8, A5);
take  h ; ::_thesis: ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h . [l2,l1] = l2 * l1 ) )
thus A11: for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h iff dom l2 = cod l1 ) ::_thesis: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h . [l2,l1] = l2 * l1
proof
let l2, l1 be Element of MapsC X; ::_thesis: ( [l2,l1] in dom h iff dom l2 = cod l1 )
thus  ( [l2,l1] in dom h implies dom l2 = cod l1 ) ::_thesis: ( dom l2 = cod l1 implies [l2,l1] in dom h )
proof
assume  [l2,l1] in dom h ; ::_thesis: dom l2 = cod l1
then  ex z being set st S1[l2,l1,z] by A9;
hence  dom l2 = cod l1 ; ::_thesis: verum
end;
assume  dom l2 = cod l1 ; ::_thesis: [l2,l1] in dom h
then  S1[l2,l1,l2 * l1] ;
hence  [l2,l1] in dom h by A9; ::_thesis: verum
end;
let l2, l1 be Element of MapsC X; ::_thesis: ( dom l2 = cod l1 implies h . [l2,l1] = l2 * l1 )
assume  dom l2 = cod l1 ; ::_thesis: h . [l2,l1] = l2 * l1
then  [l2,l1] in dom h by A11;
then  S1[l2,l1,h . (l2,l1)] by A10;
hence  h . [l2,l1] = l2 * l1 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) holds
b1 = b2
proof
let h1, h2 be PartFunc of [:(MapsC X),(MapsC X):],(MapsC X); ::_thesis: ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h2 . [l2,l1] = l2 * l1 ) implies h1 = h2 )
assume that
A12: for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h1 iff dom l2 = cod l1 ) and
A13: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h1 . [l2,l1] = l2 * l1 and
A14: for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h2 iff dom l2 = cod l1 ) and
A15: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h2 . [l2,l1] = l2 * l1 ; ::_thesis: h1 = h2
A16: dom h1 = dom h2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in dom h1 or [x,y] in dom h2 ) & ( not [x,y] in dom h2 or [x,y] in dom h1 ) )
thus  ( [x,y] in dom h1 implies [x,y] in dom h2 ) ::_thesis: ( not [x,y] in dom h2 or [x,y] in dom h1 )
proof
assume A17: [x,y] in dom h1 ; ::_thesis: [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 A12, A17;
hence  [x,y] in dom h2 by A14; ::_thesis: verum
end;
assume A18: [x,y] in dom h2 ; ::_thesis: [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 A14, A18;
hence  [x,y] in dom h1 by A12; ::_thesis: verum
end;
now__::_thesis:_for_l_being_Element_of_[:(MapsC_X),(MapsC_X):]_st_l_in_dom_h1_holds_
h1_._l_=_h2_._l
let l be Element of [:(MapsC X),(MapsC X):]; ::_thesis: ( l in dom h1 implies h1 . l = h2 . l )
assume A19: l in dom h1 ; ::_thesis: h1 . l = h2 . l
consider l2, l1 being 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; ::_thesis: verum
end;
hence  h1 = h2 by A16, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines CDom COH_SP:def_11_:_
 for X being set
for b2 being Function of (MapsC X),(CSp X) holds
( b2 = CDom X iff for l being Element of MapsC X holds b2 . l = dom l );

:: deftheorem Def12 defines CCod COH_SP:def_12_:_
 for X being set
for b2 being Function of (MapsC X),(CSp X) holds
( b2 = CCod X iff for l being Element of MapsC X holds b2 . l = cod l );

:: deftheorem Def13 defines CComp COH_SP:def_13_:_
 for X being set
for b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) holds
( b2 = CComp X iff ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) ) );

theorem :: COH_SP:26
canceled;

definition
canceled;
let X be set ;
func CohCat X ->  non empty non void strict CatStr  equals :: COH_SP:def 15
 CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);
coherence
 CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #) is non empty non void strict CatStr ;
end;

:: deftheorem  COH_SP:def_14_:_
canceled;

:: deftheorem  defines CohCat COH_SP:def_15_:_
 for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);

registration
let X be set ;
cluster CohCat X ->  non empty non void strict Category-like transitive associative reflexive ;
coherence
 ( CohCat X is Category-like & CohCat X is transitive & CohCat X is associative & CohCat X is reflexive )
proof
set M = MapsC X;
set d = CDom X;
set c = CCod X;
set p = CComp X;
set C = CohCat X;
thus P1: CohCat X is Category-like ::_thesis: ( CohCat X is transitive & CohCat X is associative & CohCat X is reflexive )
proof
let ff, gg be Morphism of (CohCat X); :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in proj1 the Comp of (CohCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (CohCat X) ) )
reconsider f = ff, g = gg as Element of MapsC X ;
 ( (CDom X) . gg = dom g & (CCod X) . ff = cod f ) by Def11, Def12;
hence  ( ( not [gg,ff] in proj1 the Comp of (CohCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (CohCat X) ) ) by Def13; ::_thesis: verum
end;
thus P2: CohCat X is transitive ::_thesis: ( CohCat X is associative & CohCat X is reflexive )
proof
let ff, gg be Morphism of (CohCat X); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A1: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
 [gg,ff] in dom the Comp of (CohCat X) by A1, P1, CAT_1:def_6;
then U: the Comp of (CohCat X) . (gg,ff) = gg (*) ff by CAT_1:def_1;
reconsider f = ff, g = gg as Element of MapsC X ;
A2: ( (CDom X) . g = dom g & (CCod X) . f = cod f ) by Def11, Def12;
then A3: (CComp X) . [g,f] = g * f by A1, Def13;
A4: ( (CDom X) . f = dom f & (CCod X) . g = cod g ) by Def11, Def12;
 ( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th22;
hence  ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A3, A4, Def11, Def12, U; ::_thesis: verum
end;
thus  CohCat X is associative ::_thesis: CohCat X is reflexive
proof
let ff, gg, hh be Morphism of (CohCat X); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
assume that
A5: dom hh = cod gg and
A6: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
reconsider f = ff, g = gg, h = hh as Element of MapsC X ;
A7: ( dom h = (CDom X) . h & cod g = (CCod X) . g ) by Def11, Def12;
then A8: dom (h * g) = dom g by A5, Th22;
A9: ( dom g = (CDom X) . g & cod f = (CCod X) . f ) by Def11, Def12;
then A10: cod (g * f) = dom h by A5, A6, A7, Th22;
 [hh,gg] in dom the Comp of (CohCat X) by P1, CAT_1:def_6, A5;
then X2: hh (*) gg = the Comp of (CohCat X) . (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 (CohCat X) by P1, CAT_1:def_6, A6;
 [gg,ff] in dom the Comp of (CohCat X) by P1, CAT_1:def_6, A6;
then X1: gg (*) ff = the Comp of (CohCat X) . (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 (CohCat X) by P1, CAT_1:def_6, A5;
hence hh (*) (gg (*) ff) = the Comp of (CohCat X) . (hh,( the Comp of (CohCat X) . (gg,ff))) by X1, CAT_1:def_1
.= (CComp X) . [h,(g * f)] by A6, A9, Def13
.= h * (g * f) by A10, Def13
.= (h * g) * f by A5, A6, A7, A9, Th23
.= (CComp X) . [(h * g),f] by A6, A9, A8, Def13
.= the Comp of (CohCat X) . (( the Comp of (CohCat X) . (hh,gg)),ff) by A5, A7, Def13
.= (hh (*) gg) (*) ff by X2, X3, CAT_1:def_1 ;
::_thesis: verum
end;
let a be Object of (CohCat X); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {}
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  id$ aa in Hom (a,a) by A12;
hence  Hom (a,a) <> {} ; ::_thesis: verum
end;
end;

LmX:  for X being set
for a being Element of (CohCat X)
for aa being Element of CSp X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
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 X be set ; ::_thesis: for a being Element of (CohCat X)
for aa being Element of CSp X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
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 ) )
let a be Element of (CohCat X); ::_thesis: for aa being Element of CSp X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
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 ) )
let aa be Element of CSp X; ::_thesis: ( a = aa implies for i being Morphism of a,a st i = id$ aa holds
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 ) ) )
assume Z1: a = aa ; ::_thesis: for i being Morphism of a,a st i = id$ aa holds
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 ) )
let i be Morphism of a,a; ::_thesis: ( i = id$ aa implies 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 ) ) )
assume Z2: i = id$ aa ; ::_thesis: 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 ) )
let b be Element of (CohCat X); ::_thesis: ( ( 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 ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
proof
assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g
let g be Morphism of a,b; ::_thesis: g (*) i = g
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 ;
::_thesis: verum
end;
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum
proof
assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f
let g be Morphism of b,a; ::_thesis: i (*) g = g
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 ;
::_thesis: verum
end;
end;

registration
let X be set ;
cluster CohCat X ->  non empty non void strict with_identities ;
coherence
 CohCat X is with_identities
proof
let a be Element of (CohCat X); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (CohCat X) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
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 = ii as Morphism of a,a by CAT_1:def_5;
take  ii ; ::_thesis: for b1 being Element of the carrier of (CohCat X) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
thus  for b1 being Element of the carrier of (CohCat X) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by LmX; ::_thesis: verum
end;
end;

begin

definition
let X be set ;
func Toler X ->  set  means :Def16: :: COH_SP:def 16
 for x being set holds
( x in it iff x is Tolerance of X );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is Tolerance of X )
proof
defpred S1[ set ] means $1 is Tolerance of X;
consider a being set  such that
A1: for x being set holds
( x in a iff ( x in bool [:X,X:] & S1[x] ) ) from XBOOLE_0:sch_1();
take  a ; ::_thesis: for x being set holds
( x in a iff x is Tolerance of X )
let x be set ; ::_thesis: ( x in a iff x is Tolerance of X )
thus  ( x in a implies x is Tolerance of X ) by A1; ::_thesis: ( x is Tolerance of X implies x in a )
assume  x is Tolerance of X ; ::_thesis: x in a
hence  x in a by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Tolerance of X ) ) & ( for x being set holds
( x in b2 iff x is Tolerance of X ) ) holds
b1 = b2
proof
let a, b be set ; ::_thesis: ( ( for x being set holds
( x in a iff x is Tolerance of X ) ) & ( for x being set holds
( x in b iff x is Tolerance of X ) ) implies a = b )
assume that
A2: for x being set holds
( x in a iff x is Tolerance of X ) and
A3: for x being set holds
( x in b iff x is Tolerance of X ) ; ::_thesis: a = b
now__::_thesis:_for_x_being_set_holds_
(_x_in_a_iff_x_in_b_)
let x be set ; ::_thesis: ( x in a iff x in b )
A4: now__::_thesis:_(_x_in_b_implies_x_in_a_)
assume  x in b ; ::_thesis: x in a
then  x is Tolerance of X by A3;
hence  x in a by A2; ::_thesis: verum
end;
now__::_thesis:_(_x_in_a_implies_x_in_b_)
assume  x in a ; ::_thesis: x in b
then  x is Tolerance of X by A2;
hence  x in b by A3; ::_thesis: verum
end;
hence  ( x in a iff x in b ) by A4; ::_thesis: verum
end;
hence  a = b by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines Toler COH_SP:def_16_:_
 for X, b2 being set holds
( b2 = Toler X iff for x being set holds
( x in b2 iff x is Tolerance of X ) );

registration
let X be set ;
cluster Toler X ->  non empty ;
coherence
 not Toler X is empty
proof
set T = the Tolerance of X;
 the Tolerance of X in Toler X by Def16;
hence  not Toler X is empty ; ::_thesis: verum
end;
end;

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

:: deftheorem  defines Toler_on_subsets COH_SP:def_17_:_
 for X being set holds Toler_on_subsets X = union  {  (Toler Y) where Y is Subset of X : verum  }  ;

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

theorem :: COH_SP:27
for x, X being set holds
( x in Toler_on_subsets X iff ex A being set st
( A c= X & x is Tolerance of A ) )
proof
let x, X be set ; ::_thesis: ( x in Toler_on_subsets X iff ex A being set st
( A c= X & x is Tolerance of A ) )
set f =  {  (Toler Y) where Y is Subset of X : verum  }  ;
thus  ( x in Toler_on_subsets X implies ex A being set st
( A c= X & x is Tolerance of A ) ) ::_thesis: ( ex A being set st
( A c= X & x is Tolerance of A ) implies x in Toler_on_subsets X )
proof
assume  x in Toler_on_subsets X ; ::_thesis: ex A being set st
( A c= X & x is Tolerance of A )
then consider a being set  such that
A1: x in a and
A2: a in  {  (Toler Y) where Y is Subset of X : verum  }  by TARSKI:def_4;
consider Y being Subset of X such that
A3: a = Toler Y by A2;
take  Y ; ::_thesis: ( Y c= X & x is Tolerance of Y )
thus  ( Y c= X & x is Tolerance of Y ) by A1, A3, Def16; ::_thesis: verum
end;
given A being set  such that A4: A c= X and
A5: x is Tolerance of A ; ::_thesis: x in Toler_on_subsets X
reconsider A = A as Subset of X by A4;
A6: Toler A in  {  (Toler Y) where Y is Subset of X : verum  }  ;
 x in Toler A by A5, Def16;
hence  x in Toler_on_subsets X by A6, TARSKI:def_4; ::_thesis: verum
end;

theorem :: COH_SP:28
for a being set holds Total a in Toler a by Def16;

theorem Th29: :: COH_SP:29
for X being set holds {} in Toler_on_subsets X
proof
let X be set ; ::_thesis: {} in Toler_on_subsets X
set F =  {  (Toler Y) where Y is Subset of X : verum  }  ;
 {} c= X by XBOOLE_1:2;
then A1: Toler {} in  {  (Toler Y) where Y is Subset of X : verum  }  ;
 {} in Toler {} by Def16, TOLER_1:14;
hence  {} in Toler_on_subsets X by A1, TARSKI:def_4; ::_thesis: verum
end;

theorem Th30: :: COH_SP:30
for a, X being set st a c= X holds
Total a in Toler_on_subsets X
proof
let a, X be set ; ::_thesis: ( a c= X implies Total a in Toler_on_subsets X )
set F =  {  (Toler Y) where Y is Subset of X : verum  }  ;
assume  a c= X ; ::_thesis: Total a in Toler_on_subsets X
then A1: Toler a in  {  (Toler Y) where Y is Subset of X : verum  }  ;
 Total a in Toler a by Def16;
hence  Total a in Toler_on_subsets X by A1, TARSKI:def_4; ::_thesis: verum
end;

theorem Th31: :: COH_SP:31
for a, X being set st a c= X holds
id a in Toler_on_subsets X
proof
let a, X be set ; ::_thesis: ( a c= X implies id a in Toler_on_subsets X )
set F =  {  (Toler Y) where Y is Subset of X : verum  }  ;
assume  a c= X ; ::_thesis: id a in Toler_on_subsets X
then A1: Toler a in  {  (Toler Y) where Y is Subset of X : verum  }  ;
 id a in Toler a by Def16;
hence  id a in Toler_on_subsets X by A1, TARSKI:def_4; ::_thesis: verum
end;

theorem :: COH_SP:32
for X being set holds Total X in Toler_on_subsets X by Th30;

theorem :: COH_SP:33
for X being set holds id X in Toler_on_subsets X by Th31;

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

:: deftheorem  defines TOL COH_SP:def_18_:_
 for X being set holds TOL X =  {  [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y  }  ;

registration
let X be set ;
cluster TOL X ->  non empty ;
coherence
 not TOL X is empty
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__::_thesis:_ex_m_being_set_st_m_in__{__[t,Y]_where_t_is_Element_of_Toler_on_subsets_X,_Y_is_Subset_of_X_:_t_is_Tolerance_of_Y__}_
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]; ::_thesis: m in  {  [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y  }
thus  m in  {  [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y  }  by TOLER_1:14; ::_thesis: verum
end;
hence  not TOL X is empty ; ::_thesis: verum
end;
end;


theorem :: COH_SP:34
for X being set holds [{},{}] in TOL X
proof
let X be set ; ::_thesis: [{},{}] in TOL X
 ( {} in Toler_on_subsets X & {} c= X ) by Th29, XBOOLE_1:2;
hence  [{},{}] in TOL X by TOLER_1:14; ::_thesis: verum
end;

theorem Th35: :: COH_SP:35
for a, X being set st a c= X holds
[(id a),a] in TOL X
proof
let a, X be set ; ::_thesis: ( a c= X implies [(id a),a] in TOL X )
assume A1: a c= X ; ::_thesis: [(id a),a] in TOL X
then  id a in Toler_on_subsets X by Th31;
hence  [(id a),a] in TOL X by A1; ::_thesis: verum
end;

theorem Th36: :: COH_SP:36
for a, X being set st a c= X holds
[(Total a),a] in TOL X
proof
let a, X be set ; ::_thesis: ( a c= X implies [(Total a),a] in TOL X )
assume A1: a c= X ; ::_thesis: [(Total a),a] in TOL X
then  Total a in Toler_on_subsets X by Th30;
hence  [(Total a),a] in TOL X by A1; ::_thesis: verum
end;

theorem :: COH_SP:37
for X being set holds [(id X),X] in TOL X by Th35;

theorem :: COH_SP:38
for X being set holds [(Total X),X] in TOL X by Th36;

definition
let X be set ;
let T be Element of TOL X;
:: original: `2
redefine funcT `2  ->  Subset of X;
coherence
 T `2 is Subset of X
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 being Element of Toler_on_subsets X, Y being Subset of X such that
W: ( T = [t,Y] & t is Tolerance of Y ) ;
 [t,Y] `2 = Y ;
hence  T `2 is Subset of X by W; ::_thesis: verum
end;
:: original: `1
redefine funcT `1  ->  Tolerance of (T `2);
coherence
 T `1 is Tolerance of (T `2)
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 being Element of Toler_on_subsets X, Y being 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  T `1 is Tolerance of (T `2) by A1, A2; ::_thesis: verum
end;
end;

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

:: deftheorem  defines FuncsT COH_SP:def_19_:_
 for X being set holds FuncsT X = union  {  (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum  }  ;

registration
let X be set ;
cluster FuncsT X ->  functional non empty ;
coherence
 ( not FuncsT X is empty & FuncsT X is functional )
proof
set F =  {  (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum  }  ;
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  {  (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum  }  ;
then reconsider UF = union  {  (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum  }  as non empty set by A1, TARSKI:def_4;
now__::_thesis:_for_f_being_set_st_f_in_UF_holds_
f_is_Function
let f be set ; ::_thesis: ( f in UF implies f is Function )
assume  f in UF ; ::_thesis: f is Function
then consider C being set  such that
A2: f in C and
A3: C in  {  (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum  }  by TARSKI:def_4;
 ex A, B being Element of TOL X st C = Funcs ((A `2),(B `2)) by A3;
hence  f is Function by A2; ::_thesis: verum
end;
hence  ( not FuncsT X is empty & FuncsT X is functional ) by FUNCT_1:def_13; ::_thesis: verum
end;
end;

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

definition
let X be set ;
func MapsT X ->  set  equals :: COH_SP:def 20
 {  [[T,TT],f] where T, 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 being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )  }  ;
coherence
  {  [[T,TT],f] where T, 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 being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )  }  is set ;
end;

:: deftheorem  defines MapsT COH_SP:def_20_:_
 for X being set holds MapsT X =  {  [[T,TT],f] where T, 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 being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )  }  ;

registration
let X be set ;
cluster MapsT X ->  non empty ;
coherence
 not MapsT X is empty
proof
set FV =  {  [[T,TT],f] where T, 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 being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )  }  ;
now__::_thesis:_ex_m_being_set_st_m_in__{__[[T,TT],f]_where_T,_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_being_set_st_[x,y]_in_T_`1_holds_
[(f_._x),(f_._y)]_in_TT_`1_)_)__}_
set a = [(Total ({} X)),({} X)];
set f = id ([(Total ({} X)),({} X)] `2);
take m = [[[(Total ({} X)),({} X)],[(Total ({} X)),({} X)]],(id ([(Total ({} X)),({} X)] `2))]; ::_thesis: m in  {  [[T,TT],f] where T, 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 being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )  }
reconsider a = [(Total ({} X)),({} X)] as Element of TOL X by Th36;
 ( a `2 = {} implies a `2 = {} ) ;
then reconsider f = id ([(Total ({} X)),({} X)] `2) as Element of FuncsT X by Th39;
 for x, y being set st [x,y] in a `1 holds
[(f . x),(f . y)] in a `1 ;
hence  m in  {  [[T,TT],f] where T, 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 being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )  }  ; ::_thesis: verum
end;
hence  not MapsT X is empty ; ::_thesis: verum
end;
end;


theorem Th40: :: COH_SP:40
for X being set
for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )
proof
let X be set ; ::_thesis: for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )
let m be Element of MapsT X; ::_thesis: ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )
 m in  {  [[T1,T2],f] where T1, T2 is Element of TOL X, f is Element of FuncsT X : ( ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )  }  ;
then  ex T1, T2 being Element of TOL X ex f being Element of FuncsT X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) ) ;
hence  ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) ) ; ::_thesis: verum
end;

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

registration
let X be set ;
let m be Element of MapsT X;
clusterm `2  ->  Relation-like Function-like ;
coherence
 ( m `2 is Function-like & m `2 is Relation-like )
proof
consider f being Element of FuncsT X, T1, T2 being 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 being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) ) by Th40;
 [[T1,T2],f] `2 = f ;
hence  ( m `2 is Function-like & m `2 is Relation-like ) by W; ::_thesis: verum
end;
end;

definition
let X be set ;
let m be Element of MapsT X;
func dom m ->  Element of TOL X equals :: COH_SP:def 21
(m `1) `1 ;
coherence
 (m `1) `1 is Element of TOL X
proof
consider f being Element of FuncsT X, T1, T2 being Element of TOL X 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 being set 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  (m `1) `1 is Element of TOL X by A1; ::_thesis: verum
end;
func cod m ->  Element of TOL X equals :: COH_SP:def 22
(m `1) `2 ;
coherence
 (m `1) `2 is Element of TOL X
proof
consider f being Element of FuncsT X, T1, T2 being Element of TOL X 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 being set 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  (m `1) `2 is Element of TOL X by A2; ::_thesis: verum
end;
end;

:: deftheorem  defines dom COH_SP:def_21_:_
 for X being set
for m being Element of MapsT X holds dom m = (m `1) `1 ;

:: deftheorem  defines cod COH_SP:def_22_:_
 for X being set
for m being Element of MapsT X holds cod m = (m `1) `2 ;

theorem Th42: :: COH_SP:42
for X being set
for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)]
proof
let X be set ; ::_thesis: for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)]
let m be Element of MapsT X; ::_thesis: m = [[(dom m),(cod m)],(m `2)]
consider f being Element of FuncsT X, T1, T2 being Element of TOL X 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 being set 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  m = [[(dom m),(cod m)],(m `2)] by A1, MCART_1:8; ::_thesis: verum
end;

Lm3:  for X being set
for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds
m = m1
proof
let X be set ; ::_thesis: for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds
m = m1
let m, m1 be Element of MapsT X; ::_thesis: ( m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 implies m = m1 )
 m = [[(dom m),(cod m)],(m `2)] by Th42;
hence  ( m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 implies m = m1 ) by Th42; ::_thesis: verum
end;

definition
let X be set ;
let T be Element of TOL X;
func id$ T ->  Element of MapsT X equals :: COH_SP:def 23
[[T,T],(id (T `2))];
coherence
 [[T,T],(id (T `2))] is Element of MapsT X
proof
set f = id (T `2);
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_T_`1_holds_
[((id_(T_`2))_._x),((id_(T_`2))_._y)]_in_T_`1
let x, y be set ; ::_thesis: ( [x,y] in T `1 implies [((id (T `2)) . x),((id (T `2)) . y)] in T `1 )
assume A1: [x,y] in T `1 ; ::_thesis: [((id (T `2)) . x),((id (T `2)) . 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  [((id (T `2)) . x),((id (T `2)) . y)] in T `1 by A1, A2, FUNCT_1:18; ::_thesis: verum
end;
hence  [[T,T],(id (T `2))] is Element of MapsT X by Th41; ::_thesis: verum
end;
end;

:: deftheorem  defines id$ COH_SP:def_23_:_
 for X being set
for T being Element of TOL X holds id$ T = [[T,T],(id (T `2))];

theorem Th43: :: COH_SP:43
for X being set
for m being Element of MapsT X holds
( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
proof
let X be set ; ::_thesis: for m being Element of MapsT X holds
( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
let m be Element of MapsT X; ::_thesis: ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
consider f being Element of FuncsT X, T1, T2 being Element of TOL X 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 being set 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; ::_thesis: for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1
let x, y be set ; ::_thesis: ( [x,y] in (dom m) `1 implies [((m `2) . x),((m `2) . y)] in (cod m) `1 )
assume  [x,y] in (dom m) `1 ; ::_thesis: [((m `2) . x),((m `2) . y)] in (cod m) `1
hence  [((m `2) . x),((m `2) . y)] in (cod m) `1 by A3, A6, A5; ::_thesis: verum
end;

definition
let X be set ;
let m1, m2 be Element of MapsT X;
assume A1: cod m1 = dom m2 ;
funcm2 * m1 ->  Element of MapsT X equals :Def24: :: COH_SP:def 24
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];
coherence
 [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X
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__::_thesis:_for_x,_y_being_set_st_[x,y]_in_(dom_m1)_`1_holds_
[(((m2_`2)_*_(m1_`2))_._x),(((m2_`2)_*_(m1_`2))_._y)]_in_(cod_m2)_`1
let x, y be set ; ::_thesis: ( [x,y] in (dom m1) `1 implies [(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `1 )
assume A6: [x,y] in (dom m1) `1 ; ::_thesis: [(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `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; ::_thesis: verum
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  [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X by A1, A3, A2, A5, Th41; ::_thesis: verum
end;
end;

:: deftheorem Def24 defines * COH_SP:def_24_:_
 for X being set
for m1, m2 being Element of MapsT X st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

theorem Th44: :: COH_SP:44
for X being set
for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
proof
let X be set ; ::_thesis: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
let m2, m1 be Element of MapsT X; ::_thesis: ( dom m2 = cod m1 implies ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) )
assume  dom m2 = cod m1 ; ::_thesis: ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
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  ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) by Lm2, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th45: :: COH_SP:45
for X being set
for m2, m1, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
proof
let X be set ; ::_thesis: for m2, m1, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
let m2, m1, m3 be Element of MapsT X; ::_thesis: ( dom m2 = cod m1 & dom m3 = cod m2 implies m3 * (m2 * m1) = (m3 * m2) * m1 )
assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2 ; ::_thesis: m3 * (m2 * m1) = (m3 * m2) * m1
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  m3 * (m2 * m1) = (m3 * m2) * m1 by A4, A7, A9, A6, A8, Lm3, RELAT_1:36; ::_thesis: verum
end;

theorem Th46: :: COH_SP:46
for X being set
for T being Element of TOL X holds
( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T )
proof
let X be set ; ::_thesis: for T being Element of TOL X holds
( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T )
let T be Element of TOL X; ::_thesis: ( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T )
 [[(dom (id$ T)),(cod (id$ T))],((id$ T) `2)] = [[T,T],(id (T `2))] by Th42;
hence  ( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T ) by Lm2, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th47: :: COH_SP:47
for X being set
for m being Element of MapsT X holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
proof
let X be set ; ::_thesis: for m being Element of MapsT X holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
let m be Element of MapsT X; ::_thesis: ( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
set i1 = id$ (dom m);
set i2 = id$ (cod m);
A1: ( (id$ (dom m)) `2 = id ((dom m) `2) & dom (id$ (dom m)) = 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 (id$ (dom m)) = dom m by Th46;
then A6: cod (m * (id$ (dom m))) = cod m by Th44;
 ( (m * (id$ (dom m))) `2 = (m `2) * ((id$ (dom m)) `2) & dom (m * (id$ (dom m))) = dom (id$ (dom m)) ) by A5, Th44;
hence  m * (id$ (dom m)) = m by A4, A1, A6, Lm3, RELAT_1:52; ::_thesis: (id$ (cod m)) * m = m
A7: ( (id$ (cod m)) `2 = id ((cod m) `2) & cod (id$ (cod m)) = cod m ) by Th46;
A8: dom (id$ (cod m)) = cod m by Th46;
then A9: cod ((id$ (cod m)) * m) = cod (id$ (cod m)) by Th44;
 ( ((id$ (cod m)) * m) `2 = ((id$ (cod m)) `2) * (m `2) & dom ((id$ (cod m)) * m) = dom m ) by A8, Th44;
hence  (id$ (cod m)) * m = m by A3, A7, A9, Lm3, RELAT_1:53; ::_thesis: verum
end;

definition
let X be set ;
func fDom X ->  Function of (MapsT X),(TOL X) means :Def25: :: COH_SP:def 25
 for m being Element of MapsT X holds it . m = dom m;
existence
 ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = dom m
proof
deffunc H1( Element of MapsT X) ->  Element of TOL X = dom $1;
thus  ex f being Function of (MapsT X),(TOL X) st
for x being Element of MapsT X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = dom m ) & ( for m being Element of MapsT X holds b2 . m = dom m ) holds
b1 = b2
proof
let h1, h2 be Function of (MapsT X),(TOL X); ::_thesis: ( ( for m being Element of MapsT X holds h1 . m = dom m ) & ( for m being Element of MapsT X holds h2 . m = dom m ) implies h1 = h2 )
assume that
A1: for m being Element of MapsT X holds h1 . m = dom m and
A2: for m being Element of MapsT X holds h2 . m = dom m ; ::_thesis: h1 = h2
now__::_thesis:_for_m_being_Element_of_MapsT_X_holds_h1_._m_=_h2_._m
let m be Element of MapsT X; ::_thesis: h1 . m = h2 . m
thus h1 . m = dom m by A1
.= h2 . m by A2 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func fCod X ->  Function of (MapsT X),(TOL X) means :Def26: :: COH_SP:def 26
 for m being Element of MapsT X holds it . m = cod m;
existence
 ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = cod m
proof
deffunc H1( Element of MapsT X) ->  Element of TOL X = cod $1;
thus  ex f being Function of (MapsT X),(TOL X) st
for x being Element of MapsT X holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = cod m ) & ( for m being Element of MapsT X holds b2 . m = cod m ) holds
b1 = b2
proof
let h1, h2 be Function of (MapsT X),(TOL X); ::_thesis: ( ( for m being Element of MapsT X holds h1 . m = cod m ) & ( for m being Element of MapsT X holds h2 . m = cod m ) implies h1 = h2 )
assume that
A3: for m being Element of MapsT X holds h1 . m = cod m and
A4: for m being Element of MapsT X holds h2 . m = cod m ; ::_thesis: h1 = h2
now__::_thesis:_for_m_being_Element_of_MapsT_X_holds_h1_._m_=_h2_._m
let m be Element of MapsT X; ::_thesis: h1 . m = h2 . m
thus h1 . m = cod m by A3
.= h2 . m by A4 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func fComp X ->  PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) means :Def27: :: COH_SP:def 27
( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom it iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
it . [m2,m1] = m2 * m1 ) );
existence
 ex b1 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st
( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
proof
defpred S1[ set , set , set ] means  for m2, m1 being Element of MapsT X 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 & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
proof
let x, y, z1, z2 be set ; ::_thesis: ( x in MapsT X & y in MapsT X & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume  ( x in MapsT X & y in MapsT X ) ; ::_thesis: ( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 )
then reconsider m2 = x, m1 = y as Element of MapsT X ;
assume that
A6: S1[x,y,z1] and
A7: S1[x,y,z2] ; ::_thesis: z1 = z2
 z1 = m2 * m1 by A6;
hence  z1 = z2 by A7; ::_thesis: verum
end;
A8: for x, y, z being set st x in MapsT X & y in MapsT X & S1[x,y,z] holds
z in MapsT X
proof
let x, y, z be set ; ::_thesis: ( x in MapsT X & y in MapsT X & S1[x,y,z] implies z in MapsT X )
assume  ( x in MapsT X & y in MapsT X ) ; ::_thesis: ( not S1[x,y,z] or z in MapsT X )
then reconsider m2 = x, m1 = y as Element of MapsT X ;
assume  S1[x,y,z] ; ::_thesis: z in MapsT X
then  z = m2 * m1 ;
hence  z in MapsT X ; ::_thesis: verum
end;
consider h being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) such that
A9: for x, y being set holds
( [x,y] in dom h iff ( x in MapsT X & y in MapsT X & ex z being set st S1[x,y,z] ) ) and
A10: for x, y being set st [x,y] in dom h holds
S1[x,y,h . (x,y)] from BINOP_1:sch_5(A8, A5);
take  h ; ::_thesis: ( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom h iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1 ) )
thus A11: for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom h iff dom m2 = cod m1 ) ::_thesis: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1
proof
let m2, m1 be Element of MapsT X; ::_thesis: ( [m2,m1] in dom h iff dom m2 = cod m1 )
thus  ( [m2,m1] in dom h implies dom m2 = cod m1 ) ::_thesis: ( dom m2 = cod m1 implies [m2,m1] in dom h )
proof
assume  [m2,m1] in dom h ; ::_thesis: dom m2 = cod m1
then  ex z being set st S1[m2,m1,z] by A9;
hence  dom m2 = cod m1 ; ::_thesis: verum
end;
assume  dom m2 = cod m1 ; ::_thesis: [m2,m1] in dom h
then  S1[m2,m1,m2 * m1] ;
hence  [m2,m1] in dom h by A9; ::_thesis: verum
end;
let m2, m1 be Element of MapsT X; ::_thesis: ( dom m2 = cod m1 implies h . [m2,m1] = m2 * m1 )
assume  dom m2 = cod m1 ; ::_thesis: h . [m2,m1] = m2 * m1
then  [m2,m1] in dom h by A11;
then  S1[m2,m1,h . (m2,m1)] by A10;
hence  h . [m2,m1] = m2 * m1 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
proof
let h1, h2 be PartFunc of [:(MapsT X),(MapsT X):],(MapsT X); ::_thesis: ( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom h1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom h2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h2 . [m2,m1] = m2 * m1 ) implies h1 = h2 )
assume that
A12: for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom h1 iff dom m2 = cod m1 ) and
A13: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h1 . [m2,m1] = m2 * m1 and
A14: for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom h2 iff dom m2 = cod m1 ) and
A15: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h2 . [m2,m1] = m2 * m1 ; ::_thesis: h1 = h2
A16: dom h1 = dom h2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in dom h1 or [x,y] in dom h2 ) & ( not [x,y] in dom h2 or [x,y] in dom h1 ) )
thus  ( [x,y] in dom h1 implies [x,y] in dom h2 ) ::_thesis: ( not [x,y] in dom h2 or [x,y] in dom h1 )
proof
assume A17: [x,y] in dom h1 ; ::_thesis: [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 A12, A17;
hence  [x,y] in dom h2 by A14; ::_thesis: verum
end;
assume A18: [x,y] in dom h2 ; ::_thesis: [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 A14, A18;
hence  [x,y] in dom h1 by A12; ::_thesis: verum
end;
now__::_thesis:_for_m_being_Element_of_[:(MapsT_X),(MapsT_X):]_st_m_in_dom_h1_holds_
h1_._m_=_h2_._m
let m be Element of [:(MapsT X),(MapsT X):]; ::_thesis: ( m in dom h1 implies h1 . m = h2 . m )
assume A19: m in dom h1 ; ::_thesis: h1 . m = h2 . m
consider m2, m1 being 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; ::_thesis: verum
end;
hence  h1 = h2 by A16, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def25 defines fDom COH_SP:def_25_:_
 for X being set
for b2 being Function of (MapsT X),(TOL X) holds
( b2 = fDom X iff for m being Element of MapsT X holds b2 . m = dom m );

:: deftheorem Def26 defines fCod COH_SP:def_26_:_
 for X being set
for b2 being Function of (MapsT X),(TOL X) holds
( b2 = fCod X iff for m being Element of MapsT X holds b2 . m = cod m );

:: deftheorem Def27 defines fComp COH_SP:def_27_:_
 for X being set
for b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) holds
( b2 = fComp X iff ( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) ) );

definition
canceled;
let X be set ;
func TolCat X ->  non empty non void strict CatStr  equals :: COH_SP:def 29
 CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);
coherence
 CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #) is non empty non void strict CatStr ;
end;

:: deftheorem  COH_SP:def_28_:_
canceled;

:: deftheorem  defines TolCat COH_SP:def_29_:_
 for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);

registration
let X be set ;
cluster TolCat X ->  non empty non void strict Category-like transitive associative reflexive ;
coherence
 ( TolCat X is Category-like & TolCat X is transitive & TolCat X is associative & TolCat X is reflexive )
proof
set C = TolCat X;
set M = MapsT X;
set d = fDom X;
set c = fCod X;
set p = fComp X;
thus P1: TolCat X is Category-like ::_thesis: ( TolCat X is transitive & TolCat X is associative & TolCat X is reflexive )
proof
let ff, gg be Morphism of (TolCat X); :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in proj1 the Comp of (TolCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (TolCat X) ) )
reconsider f = ff, g = gg as Element of MapsT X ;
 ( (fDom X) . g = dom g & (fCod X) . f = cod f ) by Def25, Def26;
hence  ( ( not [gg,ff] in proj1 the Comp of (TolCat X) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of (TolCat X) ) ) by Def27; ::_thesis: verum
end;
thus P2: TolCat X is transitive ::_thesis: ( TolCat X is associative & TolCat X is reflexive )
proof
let ff, gg be Morphism of (TolCat X); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A1: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
 [gg,ff] in dom the Comp of (TolCat X) by A1, P1, CAT_1:def_6;
then U: the Comp of (TolCat X) . (gg,ff) = gg (*) ff by CAT_1:def_1;
reconsider f = ff, g = gg as Element of MapsT X ;
A2: ( (fDom X) . g = dom g & (fCod X) . f = cod f ) by Def25, Def26;
then A3: (fComp X) . [g,f] = g * f by A1, Def27;
A4: ( (fDom X) . f = dom f & (fCod X) . g = cod g ) by Def25, Def26;
 ( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th44;
hence  ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A3, A4, Def25, Def26, U; ::_thesis: verum
end;
thus  TolCat X is associative ::_thesis: TolCat X is reflexive
proof
let ff, gg, hh be Morphism of (TolCat X); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
assume that
A5: dom hh = cod gg and
A6: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
reconsider f = ff, g = gg, h = hh as Element of MapsT X ;
A7: ( dom h = (fDom X) . h & cod g = (fCod X) . g ) by Def25, Def26;
then A8: dom (h * g) = dom g by A5, Th44;
A9: ( dom g = (fDom X) . g & cod f = (fCod X) . f ) by Def25, Def26;
then A10: cod (g * f) = dom h by A5, A6, A7, Th44;
 [hh,gg] in dom the Comp of (TolCat X) by A5, P1, CAT_1:def_6;
then X2: hh (*) gg = the Comp of (TolCat X) . (hh,gg) by CAT_1:def_1;
 [gg,ff] in dom the Comp of (TolCat X) by A6, P1, CAT_1:def_6;
then X1: gg (*) ff = the Comp of (TolCat X) . (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 (TolCat X) 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 (TolCat X) by P1, CAT_1:def_6, A5;
hence hh (*) (gg (*) ff) = the Comp of (TolCat X) . (hh,( the Comp of (TolCat X) . (gg,ff))) by X1, CAT_1:def_1
.= (fComp X) . [h,(g * f)] by A6, A9, Def27
.= h * (g * f) by A10, Def27
.= (h * g) * f by A5, A6, A7, A9, Th45
.= (fComp X) . [(h * g),f] by A6, A9, A8, Def27
.= the Comp of (TolCat X) . (( the Comp of (TolCat X) . (hh,gg)),ff) by A5, A7, Def27
.= (hh (*) gg) (*) ff by X2, X3, CAT_1:def_1 ;
::_thesis: verum
end;
let a be Object of (TolCat X); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {}
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  id$ aa in Hom (a,a) by A12;
hence  Hom (a,a) <> {} ; ::_thesis: verum
end;
end;

LmX:  for X being set
for a being Element of (TolCat X)
for aa being Element of TOL X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
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 X be set ; ::_thesis: for a being Element of (TolCat X)
for aa being Element of TOL X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
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 ) )
let a be Element of (TolCat X); ::_thesis: for aa being Element of TOL X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
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 ) )
let aa be Element of TOL X; ::_thesis: ( a = aa implies for i being Morphism of a,a st i = id$ aa holds
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 ) ) )
assume Z1: a = aa ; ::_thesis: for i being Morphism of a,a st i = id$ aa holds
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 ) )
let i be Morphism of a,a; ::_thesis: ( i = id$ aa implies 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 ) ) )
assume Z2: i = id$ aa ; ::_thesis: 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 ) )
let b be Element of (TolCat X); ::_thesis: ( ( 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 ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
proof
assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g
let g be Morphism of a,b; ::_thesis: g (*) i = g
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 ;
::_thesis: verum
end;
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum
proof
assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f
let g be Morphism of b,a; ::_thesis: i (*) g = g
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 ;
::_thesis: verum
end;
end;

registration
let X be set ;
cluster TolCat X ->  non empty non void strict with_identities ;
coherence
 TolCat X is with_identities
proof
let a be Element of (TolCat X); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (TolCat X) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
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 = ii as Morphism of a,a by CAT_1:def_5;
take  ii ; ::_thesis: for b1 being Element of the carrier of (TolCat X) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
thus  for b1 being Element of the carrier of (TolCat X) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by LmX; ::_thesis: verum
end;
end;