:: ALTCAT_1 semantic presentation

begin


theorem Th1: :: ALTCAT_1:1
for A being set holds id A in Funcs (A,A)
proof
let A be set ; ::_thesis: id A in Funcs (A,A)
 ( dom (id A) = A & rng (id A) = A ) ;
hence  id A in Funcs (A,A) by FUNCT_2:def_2; ::_thesis: verum
end;

theorem Th2: :: ALTCAT_1:2
Funcs ({},{}) = {(id {})}
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(id {})} c= Funcs ({},{})
let f be set ; ::_thesis: ( f in Funcs ({},{}) implies f in {(id {})} )
assume  f in Funcs ({},{}) ; ::_thesis: f in {(id {})}
then reconsider f9 = f as Function of {},{} by FUNCT_2:66;
 f9 = id {} ;
hence  f in {(id {})} by TARSKI:def_1; ::_thesis: verum
end;
 id {} in Funcs ({},{}) by Th1;
hence  {(id {})} c= Funcs ({},{}) by ZFMISC_1:31; ::_thesis: verum
end;

theorem Th3: :: ALTCAT_1:3
for A, B, C being set
for f, g being Function st f in Funcs (A,B) & g in Funcs (B,C) holds
g * f in Funcs (A,C)
proof
let A, B, C be set ; ::_thesis: for f, g being Function st f in Funcs (A,B) & g in Funcs (B,C) holds
g * f in Funcs (A,C)
let f, g be Function; ::_thesis: ( f in Funcs (A,B) & g in Funcs (B,C) implies g * f in Funcs (A,C) )
assume that
A1: f in Funcs (A,B) and
A2: g in Funcs (B,C) ; ::_thesis: g * f in Funcs (A,C)
A3: ex g9 being Function st
( g9 = g & dom g9 = B & rng g9 c= C ) by A2, FUNCT_2:def_2;
 rng (g * f) c= rng g by RELAT_1:26;
then A4: rng (g * f) c= C by A3, XBOOLE_1:1;
 ex f9 being Function st
( f9 = f & dom f9 = A & rng f9 c= B ) by A1, FUNCT_2:def_2;
then  dom (g * f) = A by A3, RELAT_1:27;
hence  g * f in Funcs (A,C) by A4, FUNCT_2:def_2; ::_thesis: verum
end;

theorem Th4: :: ALTCAT_1:4
for A, B, C being set st Funcs (A,B) <> {} & Funcs (B,C) <> {} holds
Funcs (A,C) <> {}
proof
let A, B, C be set ; ::_thesis: ( Funcs (A,B) <> {} & Funcs (B,C) <> {} implies Funcs (A,C) <> {} )
assume that
A1: Funcs (A,B) <> {} and
A2: Funcs (B,C) <> {} ; ::_thesis: Funcs (A,C) <> {}
consider g being set  such that
A3: g in Funcs (B,C) by A2, XBOOLE_0:def_1;
 ex f being set st f in Funcs (A,B) by A1, XBOOLE_0:def_1;
hence  Funcs (A,C) <> {} by A3, Th3; ::_thesis: verum
end;

theorem :: ALTCAT_1:5
for A, B being set
for F being ManySortedSet of [:B,A:]
for C being Subset of A
for D being Subset of B
for x, y being set st x in C & y in D holds
F . (y,x) = (F | [:D,C:]) . (y,x)
proof
let A, B be set ; ::_thesis: for F being ManySortedSet of [:B,A:]
for C being Subset of A
for D being Subset of B
for x, y being set st x in C & y in D holds
F . (y,x) = (F | [:D,C:]) . (y,x)
let F be ManySortedSet of [:B,A:]; ::_thesis: for C being Subset of A
for D being Subset of B
for x, y being set st x in C & y in D holds
F . (y,x) = (F | [:D,C:]) . (y,x)
let C be Subset of A; ::_thesis: for D being Subset of B
for x, y being set st x in C & y in D holds
F . (y,x) = (F | [:D,C:]) . (y,x)
let D be Subset of B; ::_thesis: for x, y being set st x in C & y in D holds
F . (y,x) = (F | [:D,C:]) . (y,x)
let x, y be set ; ::_thesis: ( x in C & y in D implies F . (y,x) = (F | [:D,C:]) . (y,x) )
assume  ( x in C & y in D ) ; ::_thesis: F . (y,x) = (F | [:D,C:]) . (y,x)
then  [y,x] in [:D,C:] by ZFMISC_1:87;
hence  F . (y,x) = (F | [:D,C:]) . (y,x) by FUNCT_1:49; ::_thesis: verum
end;

scheme :: ALTCAT_1:sch 1
MSSLambda2{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2():] st
for i, j being set st i in F1() & j in F2() holds
M . (i,j) = F3(i,j)
proof
deffunc H1( set ) ->  set = F3(($1 `1),($1 `2));
consider f being Function such that
A1: dom f = [:F1(),F2():] and
A2: for x being set st x in [:F1(),F2():] holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of [:F1(),F2():] by A1, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for i, j being set st i in F1() & j in F2() holds
f . (i,j) = F3(i,j)
let i, j be set ; ::_thesis: ( i in F1() & j in F2() implies f . (i,j) = F3(i,j) )
assume  ( i in F1() & j in F2() ) ; ::_thesis: f . (i,j) = F3(i,j)
then A3: [i,j] in [:F1(),F2():] by ZFMISC_1:87;
 ( [i,j] `1 = i & [i,j] `2 = j ) ;
hence  f . (i,j) = F3(i,j) by A2, A3; ::_thesis: verum
end;

scheme :: ALTCAT_1:sch 2
MSSLambda2D{ F1() ->  non empty set , F2() ->  non empty set , F3( set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2():] st
for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F3(i,j)
proof
consider M being ManySortedSet of [:F1(),F2():] such that
A1: for i, j being set st i in F1() & j in F2() holds
M . (i,j) = F3(i,j) from ALTCAT_1:sch_1();
take  M ; ::_thesis: for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F3(i,j)
thus  for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F3(i,j) by A1; ::_thesis: verum
end;

scheme :: ALTCAT_1:sch 3
MSSLambda3{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2(),F3():] st
for i, j, k being set st i in F1() & j in F2() & k in F3() holds
M . (i,j,k) = F4(i,j,k)
proof
deffunc H1( set ) ->  set = F4((($1 `1) `1),(($1 `1) `2),($1 `2));
consider f being Function such that
A1: dom f = [:F1(),F2(),F3():] and
A2: for x being set st x in [:F1(),F2(),F3():] holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of [:F1(),F2(),F3():] by A1, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for i, j, k being set st i in F1() & j in F2() & k in F3() holds
f . (i,j,k) = F4(i,j,k)
let i, j, k be set ; ::_thesis: ( i in F1() & j in F2() & k in F3() implies f . (i,j,k) = F4(i,j,k) )
A3: ( [[i,j],k] `2 = k & [i,j,k] = [[i,j],k] ) ;
A4: ([[i,j],k] `1) `2 = j ;
A5: ([[i,j],k] `1) `1 = i ;
assume  ( i in F1() & j in F2() & k in F3() ) ; ::_thesis: f . (i,j,k) = F4(i,j,k)
then A6: [i,j,k] in [:F1(),F2(),F3():] by MCART_1:69;
thus f . (i,j,k) = f . [i,j,k] by MULTOP_1:def_1
.= F4(i,j,k) by A2, A6, A5, A4, A3 ; ::_thesis: verum
end;

scheme :: ALTCAT_1:sch 4
MSSLambda3D{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set , set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2(),F3():] st
for i being Element of F1()
for j being Element of F2()
for k being Element of F3() holds M . (i,j,k) = F4(i,j,k)
proof
consider M being ManySortedSet of [:F1(),F2(),F3():] such that
A1: for i, j, k being set st i in F1() & j in F2() & k in F3() holds
M . (i,j,k) = F4(i,j,k) from ALTCAT_1:sch_3();
take  M ; ::_thesis: for i being Element of F1()
for j being Element of F2()
for k being Element of F3() holds M . (i,j,k) = F4(i,j,k)
thus  for i being Element of F1()
for j being Element of F2()
for k being Element of F3() holds M . (i,j,k) = F4(i,j,k) by A1; ::_thesis: verum
end;

theorem Th6: :: ALTCAT_1:6
for A, B being set
for N, M being ManySortedSet of [:A,B:] st ( for i, j being set st i in A & j in B holds
N . (i,j) = M . (i,j) ) holds
M = N
proof
let A, B be set ; ::_thesis: for N, M being ManySortedSet of [:A,B:] st ( for i, j being set st i in A & j in B holds
N . (i,j) = M . (i,j) ) holds
M = N
let N, M be ManySortedSet of [:A,B:]; ::_thesis: ( ( for i, j being set st i in A & j in B holds
N . (i,j) = M . (i,j) ) implies M = N )
assume A1: for i, j being set st i in A & j in B holds
N . (i,j) = M . (i,j) ; ::_thesis: M = N
A2: now__::_thesis:_for_x_being_set_st_x_in_[:A,B:]_holds_
N_._x_=_M_._x
let x be set ; ::_thesis: ( x in [:A,B:] implies N . x = M . x )
assume A3: x in [:A,B:] ; ::_thesis: N . x = M . x
then reconsider A1 = A, B1 = B as non empty set ;
consider i being Element of A1, j being Element of B1 such that
A4: x = [i,j] by A3, DOMAIN_1:1;
thus N . x = N . (i,j) by A4
.= M . (i,j) by A1
.= M . x by A4 ; ::_thesis: verum
end;
 ( dom M = [:A,B:] & dom N = [:A,B:] ) by PARTFUN1:def_2;
hence  M = N by A2, FUNCT_1:2; ::_thesis: verum
end;

theorem Th7: :: ALTCAT_1:7
for A, B being non empty set
for N, M being ManySortedSet of [:A,B:] st ( for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ) holds
M = N
proof
let A, B be non empty set ; ::_thesis: for N, M being ManySortedSet of [:A,B:] st ( for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ) holds
M = N
let N, M be ManySortedSet of [:A,B:]; ::_thesis: ( ( for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ) implies M = N )
assume  for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ; ::_thesis: M = N
then  for i, j being set st i in A & j in B holds
N . (i,j) = M . (i,j) ;
hence  M = N by Th6; ::_thesis: verum
end;

theorem Th8: :: ALTCAT_1:8
for A being set
for N, M being ManySortedSet of [:A,A,A:] st ( for i, j, k being set st i in A & j in A & k in A holds
N . (i,j,k) = M . (i,j,k) ) holds
M = N
proof
let A be set ; ::_thesis: for N, M being ManySortedSet of [:A,A,A:] st ( for i, j, k being set st i in A & j in A & k in A holds
N . (i,j,k) = M . (i,j,k) ) holds
M = N
let N, M be ManySortedSet of [:A,A,A:]; ::_thesis: ( ( for i, j, k being set st i in A & j in A & k in A holds
N . (i,j,k) = M . (i,j,k) ) implies M = N )
assume A1: for i, j, k being set st i in A & j in A & k in A holds
N . (i,j,k) = M . (i,j,k) ; ::_thesis: M = N
A2: now__::_thesis:_for_x_being_set_st_x_in_[:A,A,A:]_holds_
M_._x_=_N_._x
let x be set ; ::_thesis: ( x in [:A,A,A:] implies M . x = N . x )
assume A3: x in [:A,A,A:] ; ::_thesis: M . x = N . x
then reconsider A = A as non empty set by MCART_1:31;
consider i, j, k being Element of A such that
A4: x = [i,j,k] by A3, DOMAIN_1:3;
thus M . x = M . (i,j,k) by A4, MULTOP_1:def_1
.= N . (i,j,k) by A1
.= N . x by A4, MULTOP_1:def_1 ; ::_thesis: verum
end;
 ( dom M = [:A,A,A:] & dom N = [:A,A,A:] ) by PARTFUN1:def_2;
hence  M = N by A2, FUNCT_1:2; ::_thesis: verum
end;

theorem :: ALTCAT_1:9
for i, j, k being set holds (i,j) :-> k = [i,j] .--> k ;

theorem Th10: :: ALTCAT_1:10
for i, j, k being set holds ((i,j) :-> k) . (i,j) = k
proof
let i, j, k be set ; ::_thesis: ((i,j) :-> k) . (i,j) = k
thus ((i,j) :-> k) . (i,j) = ([i,j] .--> k) . [i,j]
.= k by FUNCOP_1:72 ; ::_thesis: verum
end;

begin

definition
attrc1 is strict ;
struct AltGraph  ->  1-sorted ;
aggrAltGraph(# carrier, Arrows #) ->  AltGraph ;
sel Arrows c1 ->  ManySortedSet of [: the carrier of c1, the carrier of c1:];
end;

definition
let G be AltGraph ;
mode object of G is Element of G;
end;

definition
let G be AltGraph ;
let o1, o2 be object of G;
func<^o1,o2^> ->  set  equals :: ALTCAT_1:def 1
 the Arrows of G . (o1,o2);
correctness
coherence
the Arrows of G . (o1,o2) is set ;
;
end;

:: deftheorem  defines <^ ALTCAT_1:def_1_:_
 for G being AltGraph
for o1, o2 being object of G holds <^o1,o2^> = the Arrows of G . (o1,o2);

definition
let G be AltGraph ;
let o1, o2 be object of G;
mode Morphism of o1,o2 is Element of <^o1,o2^>;
end;

definition
let G be AltGraph ;
attrG is transitive  means :Def2: :: ALTCAT_1:def 2
 for o1, o2, o3 being object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
<^o1,o3^> <> {} ;
end;

:: deftheorem Def2 defines transitive ALTCAT_1:def_2_:_
 for G being AltGraph holds
( G is transitive iff for o1, o2, o3 being object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
<^o1,o3^> <> {} );

begin

definition
let I be set ;
let G be ManySortedSet of [:I,I:];
func{|G|} ->  ManySortedSet of [:I,I,I:] means :Def3: :: ALTCAT_1:def 3
 for i, j, k being set st i in I & j in I & k in I holds
it . (i,j,k) = G . (i,k);
existence
 ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = G . (i,k)
proof
deffunc H1( set , set , set ) ->  set = G . ($1,$3);
 ex M being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
M . (i,j,k) = H1(i,j,k) from ALTCAT_1:sch_3();
hence  ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = G . (i,k) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . (i,j,k) = G . (i,k) ) holds
b1 = b2
proof
let M1, M2 be ManySortedSet of [:I,I,I:]; ::_thesis: ( ( for i, j, k being set st i in I & j in I & k in I holds
M1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being set st i in I & j in I & k in I holds
M2 . (i,j,k) = G . (i,k) ) implies M1 = M2 )
assume that
A1: for i, j, k being set st i in I & j in I & k in I holds
M1 . (i,j,k) = G . (i,k) and
A2: for i, j, k being set st i in I & j in I & k in I holds
M2 . (i,j,k) = G . (i,k) ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j,_k_being_set_st_i_in_I_&_j_in_I_&_k_in_I_holds_
M1_._(i,j,k)_=_M2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in I & j in I & k in I implies M1 . (i,j,k) = M2 . (i,j,k) )
assume A3: ( i in I & j in I & k in I ) ; ::_thesis: M1 . (i,j,k) = M2 . (i,j,k)
hence M1 . (i,j,k) = G . (i,k) by A1
.= M2 . (i,j,k) by A2, A3 ;
::_thesis: verum
end;
hence  M1 = M2 by Th8; ::_thesis: verum
end;
let H be ManySortedSet of [:I,I:];
func{|G,H|} ->  ManySortedSet of [:I,I,I:] means :Def4: :: ALTCAT_1:def 4
 for i, j, k being set st i in I & j in I & k in I holds
it . (i,j,k) = [:(H . (j,k)),(G . (i,j)):];
existence
 ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):]
proof
deffunc H1( set , set , set ) ->  set = [:(H . ($2,$3)),(G . ($1,$2)):];
 ex M being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
M . (i,j,k) = H1(i,j,k) from ALTCAT_1:sch_3();
hence  ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) holds
b1 = b2
proof
let M1, M2 be ManySortedSet of [:I,I,I:]; ::_thesis: ( ( for i, j, k being set st i in I & j in I & k in I holds
M1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) & ( for i, j, k being set st i in I & j in I & k in I holds
M2 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) implies M1 = M2 )
assume that
A4: for i, j, k being set st i in I & j in I & k in I holds
M1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] and
A5: for i, j, k being set st i in I & j in I & k in I holds
M2 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j,_k_being_set_st_i_in_I_&_j_in_I_&_k_in_I_holds_
M1_._(i,j,k)_=_M2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in I & j in I & k in I implies M1 . (i,j,k) = M2 . (i,j,k) )
assume A6: ( i in I & j in I & k in I ) ; ::_thesis: M1 . (i,j,k) = M2 . (i,j,k)
hence M1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] by A4
.= M2 . (i,j,k) by A5, A6 ;
::_thesis: verum
end;
hence  M1 = M2 by Th8; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines {| ALTCAT_1:def_3_:_
 for I being set
for G being ManySortedSet of [:I,I:]
for b3 being ManySortedSet of [:I,I,I:] holds
( b3 = {|G|} iff for i, j, k being set st i in I & j in I & k in I holds
b3 . (i,j,k) = G . (i,k) );

:: deftheorem Def4 defines {| ALTCAT_1:def_4_:_
 for I being set
for G, H being ManySortedSet of [:I,I:]
for b4 being ManySortedSet of [:I,I,I:] holds
( b4 = {|G,H|} iff for i, j, k being set st i in I & j in I & k in I holds
b4 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] );

definition
let I be set ;
let G be ManySortedSet of [:I,I:];
mode BinComp of G is ManySortedFunction of {|G,G|},{|G|};
end;

definition
let I be non empty set ;
let G be ManySortedSet of [:I,I:];
let o be BinComp of G;
let i, j, k be Element of I;
:: original: .
redefine funco . (i,j,k) ->  Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k));
coherence
 o . (i,j,k) is Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k))
proof
A1: {|G|} . [i,j,k] = {|G|} . (i,j,k) by MULTOP_1:def_1
.= G . (i,k) by Def3 ;
A2: o . [i,j,k] = o . (i,j,k) by MULTOP_1:def_1;
{|G,G|} . [i,j,k] = {|G,G|} . (i,j,k) by MULTOP_1:def_1
.= [:(G . (j,k)),(G . (i,j)):] by Def4 ;
hence  o . (i,j,k) is Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k)) by A2, A1, PBOOLE:def_15; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let G be ManySortedSet of [:I,I:];
let IT be BinComp of G;
attrIT is associative  means :Def5: :: ALTCAT_1:def 5
 for i, j, k, l being Element of I
for f, g, h being set st f in G . (i,j) & g in G . (j,k) & h in G . (k,l) holds
(IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f);
attrIT is with_right_units  means :Def6: :: ALTCAT_1:def 6
 for i being Element of I ex e being set st
( e in G . (i,i) & ( for j being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,i,j)) . (f,e) = f ) );
attrIT is with_left_units  means :Def7: :: ALTCAT_1:def 7
 for j being Element of I ex e being set st
( e in G . (j,j) & ( for i being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,j,j)) . (e,f) = f ) );
end;

:: deftheorem Def5 defines associative ALTCAT_1:def_5_:_
 for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is associative iff for i, j, k, l being Element of I
for f, g, h being set st f in G . (i,j) & g in G . (j,k) & h in G . (k,l) holds
(IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f) );

:: deftheorem Def6 defines with_right_units ALTCAT_1:def_6_:_
 for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is with_right_units iff for i being Element of I ex e being set st
( e in G . (i,i) & ( for j being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,i,j)) . (f,e) = f ) ) );

:: deftheorem Def7 defines with_left_units ALTCAT_1:def_7_:_
 for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is with_left_units iff for j being Element of I ex e being set st
( e in G . (j,j) & ( for i being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,j,j)) . (e,f) = f ) ) );

begin

definition
attrc1 is strict ;
struct AltCatStr  ->  AltGraph ;
aggrAltCatStr(# carrier, Arrows, Comp #) ->  AltCatStr ;
sel Comp c1 ->  BinComp of the Arrows of c1;
end;

registration
cluster non empty strict for AltCatStr ;
existence
 ex b1 being AltCatStr st
( b1 is strict & not b1 is empty )
proof
set X = the non empty set ;
set A = the ManySortedSet of [: the non empty set , the non empty set :];
set C = the BinComp of the ManySortedSet of [: the non empty set , the non empty set :];
take  AltCatStr(# the non empty set , the ManySortedSet of [: the non empty set , the non empty set :], the BinComp of the ManySortedSet of [: the non empty set , the non empty set :] #) ; ::_thesis: ( AltCatStr(# the non empty set , the ManySortedSet of [: the non empty set , the non empty set :], the BinComp of the ManySortedSet of [: the non empty set , the non empty set :] #) is strict & not AltCatStr(# the non empty set , the ManySortedSet of [: the non empty set , the non empty set :], the BinComp of the ManySortedSet of [: the non empty set , the non empty set :] #) is empty )
thus  AltCatStr(# the non empty set , the ManySortedSet of [: the non empty set , the non empty set :], the BinComp of the ManySortedSet of [: the non empty set , the non empty set :] #) is strict ; ::_thesis: not AltCatStr(# the non empty set , the ManySortedSet of [: the non empty set , the non empty set :], the BinComp of the ManySortedSet of [: the non empty set , the non empty set :] #) is empty
thus  not the carrier of AltCatStr(# the non empty set , the ManySortedSet of [: the non empty set , the non empty set :], the BinComp of the ManySortedSet of [: the non empty set , the non empty set :] #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let C be non empty AltCatStr ;
let o1, o2, o3 be object of C;
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ;
let f be Morphism of o1,o2;
let g be Morphism of o2,o3;
funcg * f ->  Morphism of o1,o3 equals :Def8: :: ALTCAT_1:def 8
( the Comp of C . (o1,o2,o3)) . (g,f);
coherence
 ( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3
proof
reconsider H1 = <^o1,o2^>, H2 = <^o2,o3^> as non empty set by A1;
reconsider F = the Comp of C . (o1,o2,o3) as Function of [:H2,H1:],<^o1,o3^> ;
reconsider y = g as Element of H2 ;
reconsider x = f as Element of H1 ;
 F . (y,x) is Element of <^o1,o3^> ;
hence  ( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3 ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem Def8 defines * ALTCAT_1:def_8_:_
 for C being non empty AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds g * f = ( the Comp of C . (o1,o2,o3)) . (g,f);

definition
let IT be Function;
attrIT is compositional  means :Def9: :: ALTCAT_1:def 9
 for x being set st x in dom IT holds
ex f, g being Function st
( x = [g,f] & IT . x = g * f );
end;

:: deftheorem Def9 defines compositional ALTCAT_1:def_9_:_
 for IT being Function holds
( IT is compositional iff for x being set st x in dom IT holds
ex f, g being Function st
( x = [g,f] & IT . x = g * f ) );

registration
let A, B be functional set ;
cluster Relation-like [:A,B:] -defined Function-like V14([:A,B:]) Function-yielding V25() compositional for set ;
existence
 ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional
proof
percases ( A = {} or B = {} or ( A <> {} & B <> {} ) ) ;
supposeA1: ( A = {} or B = {} ) ; ::_thesis: ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional
set M = [[0]] [:A,B:];
 [[0]] [:A,B:] is Function-yielding by A1;
then reconsider M = [[0]] [:A,B:] as ManySortedFunction of [:A,B:] ;
take  M ; ::_thesis: M is compositional
let x be set ; :: according to ALTCAT_1:def_9 ::_thesis: ( x in dom M implies ex f, g being Function st
( x = [g,f] & M . x = g * f ) )
thus  ( x in dom M implies ex f, g being Function st
( x = [g,f] & M . x = g * f ) ) by A1; ::_thesis: verum
end;
suppose ( A <> {} & B <> {} ) ; ::_thesis: ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional
then reconsider A1 = A, B1 = B as functional non empty set ;
deffunc H1( Element of A1, Element of B1) ->  set = A * B;
consider M being ManySortedSet of [:A1,B1:] such that
A2: for i being Element of A1
for j being Element of B1 holds M . (i,j) = H1(i,j) from ALTCAT_1:sch_2();
 M is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 M or M . x is set )
assume  x in dom M ; ::_thesis: M . x is set
then A3: x in [:A1,B1:] by PARTFUN1:def_2;
then A4: ( x `1 in A1 & x `2 in B1 ) by MCART_1:10;
then reconsider f = x `1 , g = x `2 as Function ;
M . x = M . (f,g) by A3, MCART_1:22
.= f * g by A2, A4 ;
hence  M . x is set ; ::_thesis: verum
end;
then reconsider M = M as ManySortedFunction of [:A,B:] ;
take  M ; ::_thesis: M is compositional
let x be set ; :: according to ALTCAT_1:def_9 ::_thesis: ( x in dom M implies ex f, g being Function st
( x = [g,f] & M . x = g * f ) )
assume  x in dom M ; ::_thesis: ex f, g being Function st
( x = [g,f] & M . x = g * f )
then A5: x in [:A1,B1:] by PARTFUN1:def_2;
then A6: ( x `1 in A1 & x `2 in B1 ) by MCART_1:10;
then reconsider f = x `1 , g = x `2 as Function ;
take  g ; ::_thesis: ex g being Function st
( x = [g,g] & M . x = g * g )
take  f ; ::_thesis: ( x = [f,g] & M . x = f * g )
thus  x = [f,g] by A5, MCART_1:22; ::_thesis: M . x = f * g
thus M . x = M . (f,g) by A5, MCART_1:22
.= f * g by A2, A6 ; ::_thesis: verum
end;
end;
end;
end;

theorem Th11: :: ALTCAT_1:11
for A, B being functional set
for F being compositional ManySortedSet of [:A,B:]
for g, f being Function st g in A & f in B holds
F . (g,f) = g * f
proof
let A, B be functional set ; ::_thesis: for F being compositional ManySortedSet of [:A,B:]
for g, f being Function st g in A & f in B holds
F . (g,f) = g * f
let F be compositional ManySortedSet of [:A,B:]; ::_thesis: for g, f being Function st g in A & f in B holds
F . (g,f) = g * f
let g, f be Function; ::_thesis: ( g in A & f in B implies F . (g,f) = g * f )
assume A1: ( g in A & f in B ) ; ::_thesis: F . (g,f) = g * f
 dom F = [:A,B:] by PARTFUN1:def_2;
then  [g,f] in dom F by A1, ZFMISC_1:87;
then consider ff, gg being Function such that
A2: [g,f] = [gg,ff] and
A3: F . [g,f] = gg * ff by Def9;
 g = gg by A2, XTUPLE_0:1;
hence  F . (g,f) = g * f by A2, A3, XTUPLE_0:1; ::_thesis: verum
end;

definition
let A, B be functional set ;
func FuncComp (A,B) ->  compositional ManySortedFunction of [:B,A:] means :Def10: :: ALTCAT_1:def 10
verum;
uniqueness
 for b1, b2 being compositional ManySortedFunction of [:B,A:] holds b1 = b2
proof
let M1, M2 be compositional ManySortedFunction of [:B,A:]; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_set_st_i_in_B_&_j_in_A_holds_
M1_._(i,j)_=_M2_._(i,j)
let i, j be set ; ::_thesis: ( i in B & j in A implies M1 . (i,j) = M2 . (i,j) )
assume  ( i in B & j in A ) ; ::_thesis: M1 . (i,j) = M2 . (i,j)
then A1: [i,j] in [:B,A:] by ZFMISC_1:87;
then  [i,j] in dom M1 by PARTFUN1:def_2;
then consider f1, g1 being Function such that
A2: [i,j] = [g1,f1] and
A3: M1 . [i,j] = g1 * f1 by Def9;
 [i,j] in dom M2 by A1, PARTFUN1:def_2;
then consider f2, g2 being Function such that
A4: [i,j] = [g2,f2] and
A5: M2 . [i,j] = g2 * f2 by Def9;
 g1 = g2 by A2, A4, XTUPLE_0:1;
hence  M1 . (i,j) = M2 . (i,j) by A2, A3, A4, A5, XTUPLE_0:1; ::_thesis: verum
end;
hence  M1 = M2 by Th6; ::_thesis: verum
end;
correctness
existence
ex b1 being compositional ManySortedFunction of [:B,A:] st verum;
;
end;

:: deftheorem Def10 defines FuncComp ALTCAT_1:def_10_:_
 for A, B being functional set
for b3 being compositional ManySortedFunction of [:B,A:] holds
( b3 = FuncComp (A,B) iff verum );

theorem Th12: :: ALTCAT_1:12
for A, B, C being set holds rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) c= Funcs (A,C)
proof
let A, B, C be set ; ::_thesis: rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) c= Funcs (A,C)
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) or i in Funcs (A,C) )
set F = FuncComp ((Funcs (A,B)),(Funcs (B,C)));
assume  i in rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) ; ::_thesis: i in Funcs (A,C)
then consider j being set  such that
A1: j in dom (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) and
A2: i = (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) . j by FUNCT_1:def_3;
consider f, g being Function such that
A3: j = [g,f] and
A4: (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) . j = g * f by A1, Def9;
 dom (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) = [:(Funcs (B,C)),(Funcs (A,B)):] by PARTFUN1:def_2;
then  ( g in Funcs (B,C) & f in Funcs (A,B) ) by A1, A3, ZFMISC_1:87;
hence  i in Funcs (A,C) by A2, A4, Th3; ::_thesis: verum
end;

theorem Th13: :: ALTCAT_1:13
for o being set holds FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o)
proof
let o be set ; ::_thesis: FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o)
A1: dom (FuncComp ({(id o)},{(id o)})) = [:{(id o)},{(id o)}:] by PARTFUN1:def_2;
 rng (FuncComp ({(id o)},{(id o)})) c= {(id o)}
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng (FuncComp ({(id o)},{(id o)})) or i in {(id o)} )
assume  i in rng (FuncComp ({(id o)},{(id o)})) ; ::_thesis: i in {(id o)}
then consider j being set  such that
A2: j in [:{(id o)},{(id o)}:] and
A3: i = (FuncComp ({(id o)},{(id o)})) . j by A1, FUNCT_1:def_3;
consider f, g being Function such that
A4: j = [g,f] and
A5: (FuncComp ({(id o)},{(id o)})) . j = g * f by A1, A2, Def9;
 f in {(id o)} by A2, A4, ZFMISC_1:87;
then A6: f = id o by TARSKI:def_1;
 g in {(id o)} by A2, A4, ZFMISC_1:87;
then  ( o /\ o = o & g = id o ) by TARSKI:def_1;
then  i = id o by A3, A5, A6, FUNCT_1:22;
hence  i in {(id o)} by TARSKI:def_1; ::_thesis: verum
end;
then  FuncComp ({(id o)},{(id o)}) is Function of [:{(id o)},{(id o)}:],{(id o)} by A1, RELSET_1:4;
hence  FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o) by FUNCOP_1:def_10; ::_thesis: verum
end;

theorem Th14: :: ALTCAT_1:14
for A, B being functional set
for A1 being Subset of A
for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
proof
let A, B be functional set ; ::_thesis: for A1 being Subset of A
for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
let A1 be Subset of A; ::_thesis: for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
let B1 be Subset of B; ::_thesis: FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
set f = (FuncComp (A,B)) | [:B1,A1:];
A1: dom (FuncComp (A,B)) = [:B,A:] by PARTFUN1:def_2;
then A2: dom ((FuncComp (A,B)) | [:B1,A1:]) = [:B1,A1:] by RELAT_1:62;
then reconsider f = (FuncComp (A,B)) | [:B1,A1:] as ManySortedFunction of [:B1,A1:] by PARTFUN1:def_2;
 f is compositional
proof
let i be set ; :: according to ALTCAT_1:def_9 ::_thesis: ( i in dom f implies ex f, g being Function st
( i = [g,f] & f . i = g * f ) )
assume A3: i in dom f ; ::_thesis: ex f, g being Function st
( i = [g,f] & f . i = g * f )
then  f . i = (FuncComp (A,B)) . i by A2, FUNCT_1:49;
hence  ex f, g being Function st
( i = [g,f] & f . i = g * f ) by A1, A2, A3, Def9; ::_thesis: verum
end;
hence  FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:] by Def10; ::_thesis: verum
end;

definition
let C be non empty AltCatStr ;
attrC is quasi-functional  means :Def11: :: ALTCAT_1:def 11
 for a1, a2 being object of C holds <^a1,a2^> c= Funcs (a1,a2);
attrC is semi-functional  means :Def12: :: ALTCAT_1:def 12
 for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9;
attrC is pseudo-functional  means :Def13: :: ALTCAT_1:def 13
 for o1, o2, o3 being object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:];
end;

:: deftheorem Def11 defines quasi-functional ALTCAT_1:def_11_:_
 for C being non empty AltCatStr holds
( C is quasi-functional iff for a1, a2 being object of C holds <^a1,a2^> c= Funcs (a1,a2) );

:: deftheorem Def12 defines semi-functional ALTCAT_1:def_12_:_
 for C being non empty AltCatStr holds
( C is semi-functional iff for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 );

:: deftheorem Def13 defines pseudo-functional ALTCAT_1:def_13_:_
 for C being non empty AltCatStr holds
( C is pseudo-functional iff for o1, o2, o3 being object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] );

registration
let X be non empty set ;
let A be ManySortedSet of [:X,X:];
let C be BinComp of A;
cluster AltCatStr(# X,A,C #) ->  non empty ;
coherence
 not AltCatStr(# X,A,C #) is empty ;
end;

registration
cluster non empty strict pseudo-functional for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is strict & b1 is pseudo-functional )
proof
A1: {[0,0,0]} = [:1,1,1:] by CARD_1:49, MCART_1:35;
then reconsider c = [0,0,0] .--> (FuncComp ((Funcs (0,0)),(Funcs (0,0)))) as ManySortedSet of [:1,1,1:] ;
reconsider c = c as ManySortedFunction of [:1,1,1:] ;
dom ([0,0] .--> (Funcs (0,0))) = {[0,0]} by FUNCOP_1:13
.= [:1,1:] by CARD_1:49, ZFMISC_1:29 ;
then reconsider m = [0,0] .--> (Funcs (0,0)) as ManySortedSet of [:1,1:] by PARTFUN1:def_2, RELAT_1:def_18;
A2: m . (0,0) = Funcs (0,0) by FUNCOP_1:72;
A3: 0 in 1 by CARD_1:49, TARSKI:def_1;
now__::_thesis:_for_i_being_set_st_i_in_[:1,1,1:]_holds_
c_._i_is_Function_of_({|m,m|}_._i),({|m|}_._i)
let i be set ; ::_thesis: ( i in [:1,1,1:] implies c . i is Function of ({|m,m|} . i),({|m|} . i) )
reconsider ci = c . i as Function ;
assume  i in [:1,1,1:] ; ::_thesis: c . i is Function of ({|m,m|} . i),({|m|} . i)
then A4: i = [0,0,0] by A1, TARSKI:def_1;
then A5: c . i = FuncComp ((Funcs (0,0)),(Funcs (0,0))) by FUNCOP_1:72;
then A6: dom ci = [:(m . (0,0)),(m . (0,0)):] by A2, PARTFUN1:def_2
.= {|m,m|} . (0,0,0) by A3, Def4
.= {|m,m|} . i by A4, MULTOP_1:def_1 ;
A7: {|m|} . i = {|m|} . (0,0,0) by A4, MULTOP_1:def_1
.= m . (0,0) by A3, Def3 ;
then  rng ci c= {|m|} . i by A2, A5, Th12;
hence  c . i is Function of ({|m,m|} . i),({|m|} . i) by A2, A6, A7, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
then reconsider c = c as BinComp of m by PBOOLE:def_15;
take C = AltCatStr(# 1,m,c #); ::_thesis: ( C is strict & C is pseudo-functional )
thus  C is strict ; ::_thesis: C is pseudo-functional
let o1, o2, o3 be object of C; :: according to ALTCAT_1:def_13 ::_thesis: the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
A8: o3 = 0 by CARD_1:49, TARSKI:def_1;
A9: ( o1 = 0 & o2 = 0 ) by CARD_1:49, TARSKI:def_1;
then A10: dom (FuncComp ((Funcs (0,0)),(Funcs (0,0)))) = [:<^o2,o3^>,<^o1,o2^>:] by A2, A8, PARTFUN1:def_2;
thus  the Comp of C . (o1,o2,o3) = c . [o1,o2,o3] by MULTOP_1:def_1
.= FuncComp ((Funcs (0,0)),(Funcs (0,0))) by A9, A8, FUNCOP_1:72
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A9, A8, A10, RELAT_1:68 ; ::_thesis: verum
end;
end;

theorem :: ALTCAT_1:15
for C being non empty AltCatStr
for a1, a2, a3 being object of C holds the Comp of C . (a1,a2,a3) is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^> ;

theorem Th16: :: ALTCAT_1:16
for C being non empty pseudo-functional AltCatStr
for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
proof
let C be non empty pseudo-functional AltCatStr ; ::_thesis: for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let a1, a2, a3 be object of C; ::_thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 )
assume that
A1: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) and
A2: <^a1,a3^> <> {} ; ::_thesis: for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let f be Morphism of a1,a2; ::_thesis: for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let g be Morphism of a2,a3; ::_thesis: for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let f9, g9 be Function; ::_thesis: ( f = f9 & g = g9 implies g * f = g9 * f9 )
assume A3: ( f = f9 & g = g9 ) ; ::_thesis: g * f = g9 * f9
A4: [g,f] in [:<^a2,a3^>,<^a1,a2^>:] by A1, ZFMISC_1:87;
A5: the Comp of C . (a1,a2,a3) = (FuncComp ((Funcs (a1,a2)),(Funcs (a2,a3)))) | [:<^a2,a3^>,<^a1,a2^>:] by Def13;
 ( dom ((FuncComp ((Funcs (a1,a2)),(Funcs (a2,a3)))) | [:<^a2,a3^>,<^a1,a2^>:]) c= dom (FuncComp ((Funcs (a1,a2)),(Funcs (a2,a3)))) & dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] ) by A2, FUNCT_2:def_1, RELAT_1:60;
then consider f99, g99 being Function such that
A6: [g,f] = [g99,f99] and
A7: (FuncComp ((Funcs (a1,a2)),(Funcs (a2,a3)))) . [g,f] = g99 * f99 by A5, A4, Def9;
A8: ( g = g99 & f = f99 ) by A6, XTUPLE_0:1;
thus g * f = ( the Comp of C . (a1,a2,a3)) . (g,f) by A1, Def8
.= g9 * f9 by A5, A3, A4, A7, A8, FUNCT_1:49 ; ::_thesis: verum
end;

definition
let A be non empty set ;
func EnsCat A ->  non empty strict pseudo-functional AltCatStr  means :Def14: :: ALTCAT_1:def 14
( the carrier of it = A & ( for a1, a2 being object of it holds <^a1,a2^> = Funcs (a1,a2) ) );
existence
 ex b1 being non empty strict pseudo-functional AltCatStr st
( the carrier of b1 = A & ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) )
proof
deffunc H1( set , set , set ) ->  compositional ManySortedFunction of [:(Funcs ($2,$3)),(Funcs ($1,$2)):] = FuncComp ((Funcs ($1,$2)),(Funcs ($2,$3)));
consider M being ManySortedSet of [:A,A:] such that
A1: for i, j being set st i in A & j in A holds
M . (i,j) = Funcs (i,j) from ALTCAT_1:sch_1();
consider c being ManySortedSet of [:A,A,A:] such that
A2: for i, j, k being set st i in A & j in A & k in A holds
c . (i,j,k) = H1(i,j,k) from ALTCAT_1:sch_3();
 c is Function-yielding
proof
let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in proj1 c or c . i is set )
assume  i in dom c ; ::_thesis: c . i is set
then  i in [:A,A,A:] by PARTFUN1:def_2;
then consider x1, x2, x3 being set  such that
A3: ( x1 in A & x2 in A & x3 in A ) and
A4: i = [x1,x2,x3] by MCART_1:68;
c . i = c . (x1,x2,x3) by A4, MULTOP_1:def_1
.= FuncComp ((Funcs (x1,x2)),(Funcs (x2,x3))) by A2, A3 ;
hence  c . i is set ; ::_thesis: verum
end;
then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
now__::_thesis:_for_i_being_set_st_i_in_[:A,A,A:]_holds_
c_._i_is_Function_of_({|M,M|}_._i),({|M|}_._i)
let i be set ; ::_thesis: ( i in [:A,A,A:] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )
reconsider ci = c . i as Function ;
assume  i in [:A,A,A:] ; ::_thesis: c . i is Function of ({|M,M|} . i),({|M|} . i)
then consider x1, x2, x3 being set  such that
A5: x1 in A and
A6: x2 in A and
A7: x3 in A and
A8: i = [x1,x2,x3] by MCART_1:68;
A9: {|M|} . i = {|M|} . (x1,x2,x3) by A8, MULTOP_1:def_1
.= M . (x1,x3) by A5, A6, A7, Def3 ;
A10: c . i = c . (x1,x2,x3) by A8, MULTOP_1:def_1
.= FuncComp ((Funcs (x1,x2)),(Funcs (x2,x3))) by A2, A5, A6, A7 ;
 ( M . (x1,x2) = Funcs (x1,x2) & M . (x2,x3) = Funcs (x2,x3) ) by A1, A5, A6, A7;
then A11: [:(Funcs (x2,x3)),(Funcs (x1,x2)):] = {|M,M|} . (x1,x2,x3) by A5, A6, A7, Def4
.= {|M,M|} . i by A8, MULTOP_1:def_1 ;
 M . (x1,x3) = Funcs (x1,x3) by A1, A5, A7;
then A12: rng ci c= {|M|} . i by A10, A9, Th12;
 dom ci = [:(Funcs (x2,x3)),(Funcs (x1,x2)):] by A10, PARTFUN1:def_2;
hence  c . i is Function of ({|M,M|} . i),({|M|} . i) by A11, A12, FUNCT_2:2; ::_thesis: verum
end;
then reconsider c = c as BinComp of M by PBOOLE:def_15;
set C = AltCatStr(# A,M,c #);
 AltCatStr(# A,M,c #) is pseudo-functional
proof
let o1, o2, o3 be object of AltCatStr(# A,M,c #); :: according to ALTCAT_1:def_13 ::_thesis: the Comp of AltCatStr(# A,M,c #) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
 ( <^o1,o2^> = Funcs (o1,o2) & <^o2,o3^> = Funcs (o2,o3) ) by A1;
then A13: dom (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) = [:<^o2,o3^>,<^o1,o2^>:] by PARTFUN1:def_2;
thus  the Comp of AltCatStr(# A,M,c #) . (o1,o2,o3) = FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3))) by A2
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A13, RELAT_1:68 ; ::_thesis: verum
end;
then reconsider C = AltCatStr(# A,M,c #) as non empty strict pseudo-functional AltCatStr ;
take  C ; ::_thesis: ( the carrier of C = A & ( for a1, a2 being object of C holds <^a1,a2^> = Funcs (a1,a2) ) )
thus  the carrier of C = A ; ::_thesis: for a1, a2 being object of C holds <^a1,a2^> = Funcs (a1,a2)
let a1, a2 be object of C; ::_thesis: <^a1,a2^> = Funcs (a1,a2)
thus  <^a1,a2^> = Funcs (a1,a2) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict pseudo-functional AltCatStr st the carrier of b1 = A & ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) & the carrier of b2 = A & ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) holds
b1 = b2
proof
let C1, C2 be non empty strict pseudo-functional AltCatStr ; ::_thesis: ( the carrier of C1 = A & ( for a1, a2 being object of C1 holds <^a1,a2^> = Funcs (a1,a2) ) & the carrier of C2 = A & ( for a1, a2 being object of C2 holds <^a1,a2^> = Funcs (a1,a2) ) implies C1 = C2 )
assume that
A14: the carrier of C1 = A and
A15: for a1, a2 being object of C1 holds <^a1,a2^> = Funcs (a1,a2) and
A16: the carrier of C2 = A and
A17: for a1, a2 being object of C2 holds <^a1,a2^> = Funcs (a1,a2) ; ::_thesis: C1 = C2
A18: now__::_thesis:_for_i,_j_being_set_st_i_in_A_&_j_in_A_holds_
the_Arrows_of_C1_._(i,j)_=_the_Arrows_of_C2_._(i,j)
let i, j be set ; ::_thesis: ( i in A & j in A implies the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) )
assume A19: ( i in A & j in A ) ; ::_thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
then reconsider a1 = i, a2 = j as object of C1 by A14;
reconsider b1 = i, b2 = j as object of C2 by A16, A19;
thus  the Arrows of C1 . (i,j) = <^a1,a2^>
.= Funcs (a1,a2) by A15
.= <^b1,b2^> by A17
.= the Arrows of C2 . (i,j) ; ::_thesis: verum
end;
A20: now__::_thesis:_for_i,_j,_k_being_set_st_i_in_A_&_j_in_A_&_k_in_A_holds_
the_Comp_of_C1_._(i,j,k)_=_the_Comp_of_C2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in A & j in A & k in A implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) )
assume A21: ( i in A & j in A & k in A ) ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
then reconsider a1 = i, a2 = j, a3 = k as object of C1 by A14;
reconsider b1 = i, b2 = j, b3 = k as object of C2 by A16, A21;
 ( <^a2,a3^> = <^b2,b3^> & <^a1,a2^> = <^b1,b2^> ) by A14, A18;
hence  the Comp of C1 . (i,j,k) = (FuncComp ((Funcs (b1,b2)),(Funcs (b2,b3)))) | [:<^b2,b3^>,<^b1,b2^>:] by Def13
.= the Comp of C2 . (i,j,k) by Def13 ;
::_thesis: verum
end;
 the Arrows of C1 = the Arrows of C2 by A14, A16, A18, Th6;
hence  C1 = C2 by A14, A16, A20, Th8; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines EnsCat ALTCAT_1:def_14_:_
 for A being non empty set
for b2 being non empty strict pseudo-functional AltCatStr holds
( b2 = EnsCat A iff ( the carrier of b2 = A & ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) ) );

definition
let C be non empty AltCatStr ;
attrC is associative  means :Def15: :: ALTCAT_1:def 15
 the Comp of C is associative ;
attrC is with_units  means :Def16: :: ALTCAT_1:def 16
( the Comp of C is with_left_units & the Comp of C is with_right_units );
end;

:: deftheorem Def15 defines associative ALTCAT_1:def_15_:_
 for C being non empty AltCatStr holds
( C is associative iff the Comp of C is associative );

:: deftheorem Def16 defines with_units ALTCAT_1:def_16_:_
 for C being non empty AltCatStr holds
( C is with_units iff ( the Comp of C is with_left_units & the Comp of C is with_right_units ) );

Lm1:  for A being non empty set holds
( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )
proof
let A be non empty set ; ::_thesis: ( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )
set G = the Arrows of (EnsCat A);
set C = the Comp of (EnsCat A);
thus A1: EnsCat A is transitive ::_thesis: ( EnsCat A is associative & EnsCat A is with_units )
proof
let o1, o2, o3 be object of (EnsCat A); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies <^o1,o3^> <> {} )
assume  ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: <^o1,o3^> <> {}
then  ( Funcs (o1,o2) <> {} & Funcs (o2,o3) <> {} ) by Def14;
then  Funcs (o1,o3) <> {} by Th4;
hence  <^o1,o3^> <> {} by Def14; ::_thesis: verum
end;
thus  EnsCat A is associative ::_thesis: EnsCat A is with_units
proof
let i, j, k, l be Element of (EnsCat A); :: according to ALTCAT_1:def_5,ALTCAT_1:def_15 ::_thesis: for f, g, h being set st f in the Arrows of (EnsCat A) . (i,j) & g in the Arrows of (EnsCat A) . (j,k) & h in the Arrows of (EnsCat A) . (k,l) holds
( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f)
reconsider i9 = i, j9 = j, k9 = k, l9 = l as object of (EnsCat A) ;
let f, g, h be set ; ::_thesis: ( f in the Arrows of (EnsCat A) . (i,j) & g in the Arrows of (EnsCat A) . (j,k) & h in the Arrows of (EnsCat A) . (k,l) implies ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f) )
assume that
A2: f in the Arrows of (EnsCat A) . (i,j) and
A3: g in the Arrows of (EnsCat A) . (j,k) and
A4: h in the Arrows of (EnsCat A) . (k,l) ; ::_thesis: ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f)
reconsider h99 = h as Morphism of k9,l9 by A4;
reconsider g99 = g as Morphism of j9,k9 by A3;
A5: <^k9,l9^> = Funcs (k,l) by Def14;
 ( <^i9,j9^> = Funcs (i,j) & <^j9,k9^> = Funcs (j,k) ) by Def14;
then reconsider f9 = f, g9 = g, h9 = h as Function by A2, A3, A4, A5;
A6: the Arrows of (EnsCat A) . (k,l) = <^k9,l9^> ;
A7: <^j9,k9^> <> {} by A3;
then A8: <^j9,l9^> <> {} by A1, A4, A6, Def2;
then A9: h99 * g99 = h9 * g9 by A3, A4, Th16;
reconsider f99 = f as Morphism of i9,j9 by A2;
 the Arrows of (EnsCat A) . (i,j) = <^i9,j9^> ;
then A10: <^i9,k9^> <> {} by A1, A2, A7, Def2;
then A11: g99 * f99 = g9 * f9 by A2, A3, Th16;
A12: <^i9,l9^> <> {} by A1, A4, A6, A10, Def2;
A13: ( the Comp of (EnsCat A) . (j,k,l)) . (h,g) = h99 * g99 by A3, A4, Def8;
 ( the Comp of (EnsCat A) . (i,j,k)) . (g,f) = g99 * f99 by A2, A3, Def8;
hence ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = h99 * (g99 * f99) by A4, A10, Def8
.= h9 * (g9 * f9) by A4, A10, A12, A11, Th16
.= (h9 * g9) * f9 by RELAT_1:36
.= (h99 * g99) * f99 by A2, A8, A12, A9, Th16
.= ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f) by A2, A8, A13, Def8 ;
::_thesis: verum
end;
thus  the Comp of (EnsCat A) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (EnsCat A) is with_right_units
proof
let i be Element of (EnsCat A); :: according to ALTCAT_1:def_7 ::_thesis: ex e being set st
( e in the Arrows of (EnsCat A) . (i,i) & ( for i being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . (i,i) holds
( the Comp of (EnsCat A) . (i,i,i)) . (e,f) = f ) )
reconsider i9 = i as object of (EnsCat A) ;
take  id i ; ::_thesis: ( id i in the Arrows of (EnsCat A) . (i,i) & ( for i being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . (i,i) holds
( the Comp of (EnsCat A) . (i,i,i)) . ((id i),f) = f ) )
A14: <^i9,i9^> = Funcs (i,i) by Def14;
hence  id i in the Arrows of (EnsCat A) . (i,i) by Th1; ::_thesis: for i being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . (i,i) holds
( the Comp of (EnsCat A) . (i,i,i)) . ((id i),f) = f
reconsider I = id i as Morphism of i9,i9 by A14, Th1;
let j be Element of (EnsCat A); ::_thesis: for f being set st f in the Arrows of (EnsCat A) . (j,i) holds
( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f
let f be set ; ::_thesis: ( f in the Arrows of (EnsCat A) . (j,i) implies ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f )
reconsider j9 = j as object of (EnsCat A) ;
assume A15: f in the Arrows of (EnsCat A) . (j,i) ; ::_thesis: ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f
then reconsider f99 = f as Morphism of j9,i9 ;
 <^j9,i9^> = Funcs (j,i) by Def14;
then reconsider f9 = f as Function of j,i by A15, FUNCT_2:66;
thus ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = I * f99 by A14, A15, Def8
.= (id i) * f9 by A14, A15, Th16
.= f by FUNCT_2:17 ; ::_thesis: verum
end;
let i be Element of (EnsCat A); :: according to ALTCAT_1:def_6 ::_thesis: ex e being set st
( e in the Arrows of (EnsCat A) . (i,i) & ( for j being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . (i,j) holds
( the Comp of (EnsCat A) . (i,i,j)) . (f,e) = f ) )
reconsider i9 = i as object of (EnsCat A) ;
take  id i ; ::_thesis: ( id i in the Arrows of (EnsCat A) . (i,i) & ( for j being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . (i,j) holds
( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f ) )
A16: <^i9,i9^> = Funcs (i,i) by Def14;
hence  id i in the Arrows of (EnsCat A) . (i,i) by Th1; ::_thesis: for j being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . (i,j) holds
( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f
reconsider I = id i as Morphism of i9,i9 by A16, Th1;
let j be Element of (EnsCat A); ::_thesis: for f being set st f in the Arrows of (EnsCat A) . (i,j) holds
( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f
let f be set ; ::_thesis: ( f in the Arrows of (EnsCat A) . (i,j) implies ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f )
reconsider j9 = j as object of (EnsCat A) ;
assume A17: f in the Arrows of (EnsCat A) . (i,j) ; ::_thesis: ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f
then reconsider f99 = f as Morphism of i9,j9 ;
 <^i9,j9^> = Funcs (i,j) by Def14;
then reconsider f9 = f as Function of i,j by A17, FUNCT_2:66;
thus ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f99 * I by A16, A17, Def8
.= f9 * (id i) by A16, A17, Th16
.= f by FUNCT_2:17 ; ::_thesis: verum
end;

registration
cluster non empty transitive strict associative with_units for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict )
proof
take  EnsCat {{}} ; ::_thesis: ( EnsCat {{}} is transitive & EnsCat {{}} is associative & EnsCat {{}} is with_units & EnsCat {{}} is strict )
thus  ( EnsCat {{}} is transitive & EnsCat {{}} is associative & EnsCat {{}} is with_units & EnsCat {{}} is strict ) by Lm1; ::_thesis: verum
end;
end;

theorem :: ALTCAT_1:17
for C being non empty transitive AltCatStr
for a1, a2, a3 being object of C holds
( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
proof
let C be non empty transitive AltCatStr ; ::_thesis: for a1, a2, a3 being object of C holds
( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
let a1, a2, a3 be object of C; ::_thesis: ( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
 ( not <^a1,a3^> = {} or <^a1,a2^> = {} or <^a2,a3^> = {} ) by Def2;
then  ( <^a1,a3^> = {} implies [:<^a2,a3^>,<^a1,a2^>:] = {} ) ;
hence  ( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> ) by FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum
end;

theorem Th18: :: ALTCAT_1:18
for C being non empty with_units AltCatStr
for o being object of C holds <^o,o^> <> {}
proof
let C be non empty with_units AltCatStr ; ::_thesis: for o being object of C holds <^o,o^> <> {}
let o be object of C; ::_thesis: <^o,o^> <> {}
 the Comp of C is with_left_units by Def16;
then  ex e being set st
( e in the Arrows of C . (o,o) & ( for o9 being Element of C
for f being set st f in the Arrows of C . (o9,o) holds
( the Comp of C . (o9,o,o)) . (e,f) = f ) ) by Def7;
hence  <^o,o^> <> {} ; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster EnsCat A ->  non empty transitive strict pseudo-functional associative with_units ;
coherence
 ( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units ) by Lm1;
end;

registration
cluster non empty transitive quasi-functional semi-functional  ->  non empty pseudo-functional for AltCatStr ;
coherence
 for b1 being non empty AltCatStr st b1 is quasi-functional & b1 is semi-functional & b1 is transitive holds
b1 is pseudo-functional
proof
let C be non empty AltCatStr ; ::_thesis: ( C is quasi-functional & C is semi-functional & C is transitive implies C is pseudo-functional )
assume A1: ( C is quasi-functional & C is semi-functional & C is transitive ) ; ::_thesis: C is pseudo-functional
let o1, o2, o3 be object of C; :: according to ALTCAT_1:def_13 ::_thesis: the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
set c = the Comp of C . (o1,o2,o3);
set f = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:];
percases ( <^o2,o3^> = {} or <^o1,o2^> = {} or ( <^o2,o3^> <> {} & <^o1,o2^> <> {} ) ) ;
supposeA2: ( <^o2,o3^> = {} or <^o1,o2^> = {} ) ; ::_thesis: the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
hence  the Comp of C . (o1,o2,o3) = {}
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A2 ;
::_thesis: verum
end;
supposeA3: ( <^o2,o3^> <> {} & <^o1,o2^> <> {} ) ; ::_thesis: the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
then A4: <^o1,o3^> <> {} by A1, Def2;
then A5: dom ( the Comp of C . (o1,o2,o3)) = [:<^o2,o3^>,<^o1,o2^>:] by FUNCT_2:def_1;
A6: ( <^o2,o3^> c= Funcs (o2,o3) & <^o1,o2^> c= Funcs (o1,o2) ) by A1, Def11;
 dom (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) = [:(Funcs (o2,o3)),(Funcs (o1,o2)):] by PARTFUN1:def_2;
then  dom ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) = [:(Funcs (o2,o3)),(Funcs (o1,o2)):] /\ [:<^o2,o3^>,<^o1,o2^>:] by RELAT_1:61;
then A7: dom ( the Comp of C . (o1,o2,o3)) = dom ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) by A6, A5, XBOOLE_1:28, ZFMISC_1:96;
now__::_thesis:_for_i_being_set_st_i_in_dom_(_the_Comp_of_C_._(o1,o2,o3))_holds_
(_the_Comp_of_C_._(o1,o2,o3))_._i_=_((FuncComp_((Funcs_(o1,o2)),(Funcs_(o2,o3))))_|_[:<^o2,o3^>,<^o1,o2^>:])_._i
let i be set ; ::_thesis: ( i in dom ( the Comp of C . (o1,o2,o3)) implies ( the Comp of C . (o1,o2,o3)) . i = ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) . i )
assume A8: i in dom ( the Comp of C . (o1,o2,o3)) ; ::_thesis: ( the Comp of C . (o1,o2,o3)) . i = ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) . i
then consider i1, i2 being set  such that
A9: i1 in <^o2,o3^> and
A10: i2 in <^o1,o2^> and
A11: i = [i1,i2] by A5, ZFMISC_1:84;
reconsider a2 = i2 as Morphism of o1,o2 by A10;
reconsider a1 = i1 as Morphism of o2,o3 by A9;
reconsider g = i1, h = i2 as Function by A6, A9, A10;
thus ( the Comp of C . (o1,o2,o3)) . i = ( the Comp of C . (o1,o2,o3)) . (a1,a2) by A11
.= a1 * a2 by A3, Def8
.= g * h by A1, A3, A4, Def12
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) . (g,h) by A6, A9, A10, Th11
.= ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) . i by A7, A8, A11, FUNCT_1:47 ; ::_thesis: verum
end;
hence  the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A7, FUNCT_1:2; ::_thesis: verum
end;
end;
end;
cluster non empty transitive pseudo-functional with_units  ->  non empty quasi-functional semi-functional for AltCatStr ;
coherence
 for b1 being non empty AltCatStr st b1 is with_units & b1 is pseudo-functional & b1 is transitive holds
( b1 is quasi-functional & b1 is semi-functional )
proof
let C be non empty AltCatStr ; ::_thesis: ( C is with_units & C is pseudo-functional & C is transitive implies ( C is quasi-functional & C is semi-functional ) )
assume A12: ( C is with_units & C is pseudo-functional & C is transitive ) ; ::_thesis: ( C is quasi-functional & C is semi-functional )
thus  C is quasi-functional ::_thesis: C is semi-functional
proof
let a1, a2 be object of C; :: according to ALTCAT_1:def_11 ::_thesis: <^a1,a2^> c= Funcs (a1,a2)
percases ( <^a1,a2^> = {} or <^a1,a2^> <> {} ) ;
suppose <^a1,a2^> = {} ; ::_thesis: <^a1,a2^> c= Funcs (a1,a2)
hence  <^a1,a2^> c= Funcs (a1,a2) by XBOOLE_1:2; ::_thesis: verum
end;
supposeA13: <^a1,a2^> <> {} ; ::_thesis: <^a1,a2^> c= Funcs (a1,a2)
set c = the Comp of C . (a1,a1,a2);
set f = FuncComp ((Funcs (a1,a1)),(Funcs (a1,a2)));
A14: dom ( the Comp of C . (a1,a1,a2)) = [:<^a1,a2^>,<^a1,a1^>:] by A13, FUNCT_2:def_1;
 ( dom (FuncComp ((Funcs (a1,a1)),(Funcs (a1,a2)))) = [:(Funcs (a1,a2)),(Funcs (a1,a1)):] & the Comp of C . (a1,a1,a2) = (FuncComp ((Funcs (a1,a1)),(Funcs (a1,a2)))) | [:<^a1,a2^>,<^a1,a1^>:] ) by A12, Def13, PARTFUN1:def_2;
then A15: [:<^a1,a2^>,<^a1,a1^>:] c= [:(Funcs (a1,a2)),(Funcs (a1,a1)):] by A14, RELAT_1:60;
 <^a1,a1^> <> {} by A12, Th18;
hence  <^a1,a2^> c= Funcs (a1,a2) by A13, A15, ZFMISC_1:114; ::_thesis: verum
end;
end;
end;
let a1, a2, a3 be object of C; :: according to ALTCAT_1:def_12 ::_thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 )
thus  ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 ) by A12, Th16; ::_thesis: verum
end;
end;

definition
mode category is non empty transitive associative with_units AltCatStr ;
end;

begin

definition
let C be non empty with_units AltCatStr ;
let o be object of C;
func idm o ->  Morphism of o,o means :Def17: :: ALTCAT_1:def 17
 for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * it = a;
existence
 ex b1 being Morphism of o,o st
for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b1 = a
proof
 the Comp of C is with_right_units by Def16;
then consider e being set  such that
A1: e in the Arrows of C . (o,o) and
A2: for o9 being Element of C
for f being set st f in the Arrows of C . (o,o9) holds
( the Comp of C . (o,o,o9)) . (f,e) = f by Def6;
reconsider e = e as Morphism of o,o by A1;
take  e ; ::_thesis: for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * e = a
let o9 be object of C; ::_thesis: ( <^o,o9^> <> {} implies for a being Morphism of o,o9 holds a * e = a )
assume A3: <^o,o9^> <> {} ; ::_thesis: for a being Morphism of o,o9 holds a * e = a
let a be Morphism of o,o9; ::_thesis: a * e = a
thus a * e = ( the Comp of C . (o,o,o9)) . (a,e) by A1, A3, Def8
.= a by A2, A3 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Morphism of o,o st ( for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b1 = a ) & ( for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b2 = a ) holds
b1 = b2
proof
 the Comp of C is with_left_units by Def16;
then consider d being set  such that
A4: d in the Arrows of C . (o,o) and
A5: for o9 being Element of C
for f being set st f in the Arrows of C . (o9,o) holds
( the Comp of C . (o9,o,o)) . (d,f) = f by Def7;
reconsider d = d as Morphism of o,o by A4;
let a1, a2 be Morphism of o,o; ::_thesis: ( ( for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a1 = a ) & ( for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a2 = a ) implies a1 = a2 )
assume that
A6: for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a1 = a and
A7: for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a2 = a ; ::_thesis: a1 = a2
A8: <^o,o^> <> {} by Th18;
hence a1 = ( the Comp of C . (o,o,o)) . (d,a1) by A5
.= d * a1 by A8, Def8
.= d by A6, Th18
.= d * a2 by A7, Th18
.= ( the Comp of C . (o,o,o)) . (d,a2) by A8, Def8
.= a2 by A5, A8 ;
::_thesis: verum
end;
end;

:: deftheorem Def17 defines idm ALTCAT_1:def_17_:_
 for C being non empty with_units AltCatStr
for o being object of C
for b3 being Morphism of o,o holds
( b3 = idm o iff for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b3 = a );

theorem Th19: :: ALTCAT_1:19
for C being non empty with_units AltCatStr
for o being object of C holds idm o in <^o,o^>
proof
let C be non empty with_units AltCatStr ; ::_thesis: for o being object of C holds idm o in <^o,o^>
let o be object of C; ::_thesis: idm o in <^o,o^>
 <^o,o^> <> {} by Th18;
hence  idm o in <^o,o^> ; ::_thesis: verum
end;

theorem :: ALTCAT_1:20
for C being non empty with_units AltCatStr
for o1, o2 being object of C st <^o1,o2^> <> {} holds
for a being Morphism of o1,o2 holds (idm o2) * a = a
proof
let C be non empty with_units AltCatStr ; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} holds
for a being Morphism of o1,o2 holds (idm o2) * a = a
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} implies for a being Morphism of o1,o2 holds (idm o2) * a = a )
assume A1: <^o1,o2^> <> {} ; ::_thesis: for a being Morphism of o1,o2 holds (idm o2) * a = a
let a be Morphism of o1,o2; ::_thesis: (idm o2) * a = a
 the Comp of C is with_left_units by Def16;
then consider d being set  such that
A2: d in the Arrows of C . (o2,o2) and
A3: for o9 being Element of C
for f being set st f in the Arrows of C . (o9,o2) holds
( the Comp of C . (o9,o2,o2)) . (d,f) = f by Def7;
reconsider d = d as Morphism of o2,o2 by A2;
 idm o2 in <^o2,o2^> by Th19;
then d = d * (idm o2) by Def17
.= ( the Comp of C . (o2,o2,o2)) . (d,(idm o2)) by A2, Def8
.= idm o2 by A3, Th19 ;
hence (idm o2) * a = ( the Comp of C . (o1,o2,o2)) . (d,a) by A1, A2, Def8
.= a by A1, A3 ;
::_thesis: verum
end;

theorem :: ALTCAT_1:21
for C being non empty transitive associative AltCatStr
for o1, o2, o3, o4 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
proof
let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3, o4 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
let o1, o2, o3, o4 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o4^> <> {} ; ::_thesis: for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
let a be Morphism of o1,o2; ::_thesis: for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
let b be Morphism of o2,o3; ::_thesis: for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
let c be Morphism of o3,o4; ::_thesis: c * (b * a) = (c * b) * a
A4: ( <^o2,o4^> <> {} & c * b = ( the Comp of C . (o2,o3,o4)) . (c,b) ) by A2, A3, Def2, Def8;
A5: the Comp of C is associative by Def15;
 ( <^o1,o3^> <> {} & b * a = ( the Comp of C . (o1,o2,o3)) . (b,a) ) by A1, A2, Def2, Def8;
hence c * (b * a) = ( the Comp of C . (o1,o3,o4)) . (c,(( the Comp of C . (o1,o2,o3)) . (b,a))) by A3, Def8
.= ( the Comp of C . (o1,o2,o4)) . ((( the Comp of C . (o2,o3,o4)) . (c,b)),a) by A1, A2, A3, A5, Def5
.= (c * b) * a by A1, A4, Def8 ;
::_thesis: verum
end;

begin

definition
let C be AltCatStr ;
attrC is quasi-discrete  means :Def18: :: ALTCAT_1:def 18
 for i, j being object of C st <^i,j^> <> {} holds
i = j;
attrC is pseudo-discrete  means :Def19: :: ALTCAT_1:def 19
 for i being object of C holds <^i,i^> is trivial ;
end;

:: deftheorem Def18 defines quasi-discrete ALTCAT_1:def_18_:_
 for C being AltCatStr holds
( C is quasi-discrete iff for i, j being object of C st <^i,j^> <> {} holds
i = j );

:: deftheorem Def19 defines pseudo-discrete ALTCAT_1:def_19_:_
 for C being AltCatStr holds
( C is pseudo-discrete iff for i being object of C holds <^i,i^> is trivial );

theorem :: ALTCAT_1:22
for C being non empty with_units AltCatStr holds
( C is pseudo-discrete iff for o being object of C holds <^o,o^> = {(idm o)} )
proof
let C be non empty with_units AltCatStr ; ::_thesis: ( C is pseudo-discrete iff for o being object of C holds <^o,o^> = {(idm o)} )
hereby  ::_thesis: ( ( for o being object of C holds <^o,o^> = {(idm o)} ) implies C is pseudo-discrete )
assume A1: C is pseudo-discrete ; ::_thesis: for o being object of C holds <^o,o^> = {(idm o)}
let o be object of C; ::_thesis: <^o,o^> = {(idm o)}
now__::_thesis:_for_j_being_set_holds_
(_(_j_in_<^o,o^>_implies_j_=_idm_o_)_&_(_j_=_idm_o_implies_j_in_<^o,o^>_)_)
let j be set ; ::_thesis: ( ( j in <^o,o^> implies j = idm o ) & ( j = idm o implies j in <^o,o^> ) )
hereby  ::_thesis: ( j = idm o implies j in <^o,o^> )
 ( idm o in <^o,o^> & <^o,o^> is trivial ) by A1, Def19, Th19;
then consider i being set  such that
A2: <^o,o^> = {i} by ZFMISC_1:131;
assume  j in <^o,o^> ; ::_thesis: j = idm o
then  j = i by A2, TARSKI:def_1;
hence  j = idm o by A2, TARSKI:def_1; ::_thesis: verum
end;
thus  ( j = idm o implies j in <^o,o^> ) by Th19; ::_thesis: verum
end;
hence  <^o,o^> = {(idm o)} by TARSKI:def_1; ::_thesis: verum
end;
assume A3: for o being object of C holds <^o,o^> = {(idm o)} ; ::_thesis: C is pseudo-discrete
let o be object of C; :: according to ALTCAT_1:def_19 ::_thesis: <^o,o^> is trivial
 <^o,o^> = {(idm o)} by A3;
hence  <^o,o^> is trivial ; ::_thesis: verum
end;

registration
cluster1 -element  ->  quasi-discrete for AltCatStr ;
coherence
 for b1 being AltCatStr st b1 is 1 -element holds
b1 is quasi-discrete
proof
let C be AltCatStr ; ::_thesis: ( C is 1 -element implies C is quasi-discrete )
assume A1: C is 1 -element ; ::_thesis: C is quasi-discrete
let i, j be object of C; :: according to ALTCAT_1:def_18 ::_thesis: ( <^i,j^> <> {} implies i = j )
assume  <^i,j^> <> {} ; ::_thesis: i = j
thus  i = j by A1, STRUCT_0:def_10; ::_thesis: verum
end;
end;

theorem Th23: :: ALTCAT_1:23
( EnsCat 1 is pseudo-discrete & EnsCat 1 is 1 -element )
proof
A1: the carrier of (EnsCat 1) = {{}} by Def14, CARD_1:49;
hereby  :: according to ALTCAT_1:def_19 ::_thesis: EnsCat 1 is 1 -element
let i be object of (EnsCat 1); ::_thesis: <^i,i^> is trivial
 i = {} by A1, TARSKI:def_1;
hence  <^i,i^> is trivial by Def14, Th2; ::_thesis: verum
end;
thus  the carrier of (EnsCat 1) is 1 -element by A1; :: according to STRUCT_0:def_19 ::_thesis: verum
end;

registration
cluster non empty trivial transitive strict associative with_units pseudo-discrete for AltCatStr ;
existence
 ex b1 being category st
( b1 is pseudo-discrete & b1 is trivial & b1 is strict ) by Th23;
end;

registration
cluster non empty trivial transitive strict associative with_units quasi-discrete pseudo-discrete for AltCatStr ;
existence
 ex b1 being category st
( b1 is quasi-discrete & b1 is pseudo-discrete & b1 is trivial & b1 is strict ) by Th23;
end;

definition
mode discrete_category is quasi-discrete pseudo-discrete category;
end;

definition
let A be non empty set ;
func DiscrCat A ->  non empty strict quasi-discrete AltCatStr  means :Def20: :: ALTCAT_1:def 20
( the carrier of it = A & ( for i being object of it holds <^i,i^> = {(id i)} ) );
existence
 ex b1 being non empty strict quasi-discrete AltCatStr st
( the carrier of b1 = A & ( for i being object of b1 holds <^i,i^> = {(id i)} ) )
proof
deffunc H1( Element of A, set , set ) ->  set = IFEQ ($1,$2,(IFEQ ($2,$3,([(id $1),(id $1)] .--> (id $1)),{})),{});
deffunc H2( Element of A, set ) ->  set = IFEQ ($1,$2,{(id $1)},{});
consider M being ManySortedSet of [:A,A:] such that
A1: for i, j being Element of A holds M . (i,j) = H2(i,j) from ALTCAT_1:sch_2();
consider c being ManySortedSet of [:A,A,A:] such that
A2: for i, j, k being Element of A holds c . (i,j,k) = H1(i,j,k) from ALTCAT_1:sch_4();
A3: now__::_thesis:_for_i_being_set_st_i_in_[:A,A,A:]_holds_
c_._i_is_Function_of_({|M,M|}_._i),({|M|}_._i)
let i be set ; ::_thesis: ( i in [:A,A,A:] implies c . b1 is Function of ({|M,M|} . b1),({|M|} . b1) )
assume  i in [:A,A,A:] ; ::_thesis: c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)
then consider i1, i2, i3 being set  such that
A4: ( i1 in A & i2 in A & i3 in A ) and
A5: i = [i1,i2,i3] by MCART_1:68;
reconsider i1 = i1, i2 = i2, i3 = i3 as Element of A by A4;
percases ( ( i1 = i2 & i2 = i3 ) or i1 <> i2 or i2 <> i3 ) ;
supposethat A6: i1 = i2 and
A7: i2 = i3 ; ::_thesis: c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)
A8: M . (i1,i1) = IFEQ (i1,i1,{(id i1)},{}) by A1
.= {(id i1)} by FUNCOP_1:def_8 ;
A9: c . i = c . (i1,i2,i3) by A5, MULTOP_1:def_1
.= IFEQ (i1,i2,(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),{}) by A2
.= IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{}) by A6, FUNCOP_1:def_8
.= [(id i1),(id i1)] .--> (id i1) by A7, FUNCOP_1:def_8 ;
A10: {|M|} . i = {|M|} . (i1,i1,i1) by A5, A6, A7, MULTOP_1:def_1
.= {(id i1)} by A8, Def3 ;
{|M,M|} . i = {|M,M|} . (i1,i1,i1) by A5, A6, A7, MULTOP_1:def_1
.= [:{(id i1)},{(id i1)}:] by A8, Def4
.= {[(id i1),(id i1)]} by ZFMISC_1:29
.= dom ([(id i1),(id i1)] .--> (id i1)) by FUNCOP_1:13 ;
hence  c . i is Function of ({|M,M|} . i),({|M|} . i) by A9, A10, FUNCT_2:def_1; ::_thesis: verum
end;
supposeA11: ( i1 <> i2 or i2 <> i3 ) ; ::_thesis: c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)
A12: now__::_thesis:_c_._i_=_{}
percases ( i1 <> i2 or ( i1 = i2 & i2 <> i3 ) ) by A11;
supposeA13: i1 <> i2 ; ::_thesis: c . i = {}
thus c . i = c . (i1,i2,i3) by A5, MULTOP_1:def_1
.= IFEQ (i1,i2,(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),{}) by A2
.= {} by A13, FUNCOP_1:def_8 ; ::_thesis: verum
end;
supposethat A14: i1 = i2 and
A15: i2 <> i3 ; ::_thesis: c . i = {}
thus c . i = c . (i1,i2,i3) by A5, MULTOP_1:def_1
.= IFEQ (i1,i2,(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),{}) by A2
.= IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{}) by A14, FUNCOP_1:def_8
.= {} by A15, FUNCOP_1:def_8 ; ::_thesis: verum
end;
end;
end;
 ( M . (i1,i2) = IFEQ (i1,i2,{(id i1)},{}) & M . (i2,i3) = IFEQ (i2,i3,{(id i2)},{}) ) by A1;
then A16: ( M . (i1,i2) = {} or M . (i2,i3) = {} ) by A11, FUNCOP_1:def_8;
{|M,M|} . i = {|M,M|} . (i1,i2,i3) by A5, MULTOP_1:def_1
.= [:(M . (i2,i3)),(M . (i1,i2)):] by Def4
.= {} by A16 ;
hence  c . i is Function of ({|M,M|} . i),({|M|} . i) by A12, FUNCT_2:2, RELAT_1:38, XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
 c is Function-yielding
proof
let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in proj1 c or c . i is set )
assume  i in dom c ; ::_thesis: c . i is set
then  i in [:A,A,A:] by PARTFUN1:def_2;
hence  c . i is set by A3; ::_thesis: verum
end;
then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
reconsider c = c as BinComp of M by A3, PBOOLE:def_15;
set C = AltCatStr(# A,M,c #);
 AltCatStr(# A,M,c #) is quasi-discrete
proof
let o1, o2 be object of AltCatStr(# A,M,c #); :: according to ALTCAT_1:def_18 ::_thesis: ( <^o1,o2^> <> {} implies o1 = o2 )
assume that
A17: <^o1,o2^> <> {} and
A18: o1 <> o2 ; ::_thesis: contradiction
<^o1,o2^> = IFEQ (o1,o2,{(id o1)},{}) by A1
.= {} by A18, FUNCOP_1:def_8 ;
hence  contradiction by A17; ::_thesis: verum
end;
then reconsider C = AltCatStr(# A,M,c #) as non empty strict quasi-discrete AltCatStr ;
take  C ; ::_thesis: ( the carrier of C = A & ( for i being object of C holds <^i,i^> = {(id i)} ) )
thus  the carrier of C = A ; ::_thesis: for i being object of C holds <^i,i^> = {(id i)}
let i be object of C; ::_thesis: <^i,i^> = {(id i)}
thus <^i,i^> = IFEQ (i,i,{(id i)},{}) by A1
.= {(id i)} by FUNCOP_1:def_8 ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict quasi-discrete AltCatStr st the carrier of b1 = A & ( for i being object of b1 holds <^i,i^> = {(id i)} ) & the carrier of b2 = A & ( for i being object of b2 holds <^i,i^> = {(id i)} ) holds
b1 = b2;
proof
let C1, C2 be non empty strict quasi-discrete AltCatStr ; ::_thesis: ( the carrier of C1 = A & ( for i being object of C1 holds <^i,i^> = {(id i)} ) & the carrier of C2 = A & ( for i being object of C2 holds <^i,i^> = {(id i)} ) implies C1 = C2 )
assume that
A19: the carrier of C1 = A and
A20: for i being object of C1 holds <^i,i^> = {(id i)} and
A21: the carrier of C2 = A and
A22: for i being object of C2 holds <^i,i^> = {(id i)} ; ::_thesis: C1 = C2
A23: now__::_thesis:_for_i,_j,_k_being_set_st_i_in_A_&_j_in_A_&_k_in_A_holds_
the_Comp_of_C1_._(i,j,k)_=_the_Comp_of_C2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in A & j in A & k in A implies the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3) )
assume that
A24: i in A and
A25: ( j in A & k in A ) ; ::_thesis: the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)
reconsider i2 = i as object of C2 by A21, A24;
reconsider i1 = i as object of C1 by A19, A24;
percases ( ( i = j & j = k ) or i <> j or j <> k ) ;
supposeA26: ( i = j & j = k ) ; ::_thesis: the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)
A27: ( <^i2,i2^> = {(id i2)} & the Comp of C2 . (i2,i2,i2) is Function of [:<^i2,i2^>,<^i2,i2^>:],<^i2,i2^> ) by A22;
 ( <^i1,i1^> = {(id i1)} & the Comp of C1 . (i1,i1,i1) is Function of [:<^i1,i1^>,<^i1,i1^>:],<^i1,i1^> ) by A20;
hence  the Comp of C1 . (i,j,k) = ((id i),(id i)) :-> (id i) by A26, FUNCOP_1:def_10
.= the Comp of C2 . (i,j,k) by A26, A27, FUNCOP_1:def_10 ;
::_thesis: verum
end;
supposeA28: ( i <> j or j <> k ) ; ::_thesis: the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)
reconsider j1 = j, k1 = k as object of C1 by A19, A25;
A29: ( <^i1,j1^> = {} or <^j1,k1^> = {} ) by A28, Def18;
reconsider j2 = j, k2 = k as object of C2 by A21, A25;
A30: ( the Comp of C2 . (i2,j2,k2) is Function of [:<^j2,k2^>,<^i2,j2^>:],<^i2,k2^> & the Comp of C1 . (i1,j1,k1) is Function of [:<^j1,k1^>,<^i1,j1^>:],<^i1,k1^> ) ;
 ( <^i2,j2^> = {} or <^j2,k2^> = {} ) by A28, Def18;
hence  the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A29, A30; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_i,_j_being_Element_of_A_holds_the_Arrows_of_C1_._(i,j)_=_the_Arrows_of_C2_._(i,j)
let i, j be Element of A; ::_thesis: the Arrows of C1 . (b1,b2) = the Arrows of C2 . (b1,b2)
reconsider i2 = i as object of C2 by A21;
reconsider i1 = i as object of C1 by A19;
percases ( i = j or i <> j ) ;
supposeA31: i = j ; ::_thesis: the Arrows of C1 . (b1,b2) = the Arrows of C2 . (b1,b2)
hence  the Arrows of C1 . (i,j) = <^i1,i1^>
.= {(id i)} by A20
.= <^i2,i2^> by A22
.= the Arrows of C2 . (i,j) by A31 ;
::_thesis: verum
end;
supposeA32: i <> j ; ::_thesis: the Arrows of C1 . (b1,b2) = the Arrows of C2 . (b1,b2)
reconsider j2 = j as object of C2 by A21;
reconsider j1 = j as object of C1 by A19;
thus  the Arrows of C1 . (i,j) = <^i1,j1^>
.= {} by A32, Def18
.= <^i2,j2^> by A32, Def18
.= the Arrows of C2 . (i,j) ; ::_thesis: verum
end;
end;
end;
then  the Arrows of C1 = the Arrows of C2 by A19, A21, Th7;
hence  C1 = C2 by A19, A21, A23, Th8; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines DiscrCat ALTCAT_1:def_20_:_
 for A being non empty set
for b2 being non empty strict quasi-discrete AltCatStr holds
( b2 = DiscrCat A iff ( the carrier of b2 = A & ( for i being object of b2 holds <^i,i^> = {(id i)} ) ) );

registration
cluster quasi-discrete  ->  transitive for AltCatStr ;
coherence
 for b1 being AltCatStr st b1 is quasi-discrete holds
b1 is transitive
proof
let C be AltCatStr ; ::_thesis: ( C is quasi-discrete implies C is transitive )
assume A1: C is quasi-discrete ; ::_thesis: C is transitive
let o1, o2, o3 be object of C; :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies <^o1,o3^> <> {} )
assume  ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: <^o1,o3^> <> {}
hence  <^o1,o3^> <> {} by A1, Def18; ::_thesis: verum
end;
end;

theorem Th24: :: ALTCAT_1:24
for A being non empty set
for o1, o2, o3 being object of (DiscrCat A) st ( o1 <> o2 or o2 <> o3 ) holds
the Comp of (DiscrCat A) . (o1,o2,o3) = {}
proof
let A be non empty set ; ::_thesis: for o1, o2, o3 being object of (DiscrCat A) st ( o1 <> o2 or o2 <> o3 ) holds
the Comp of (DiscrCat A) . (o1,o2,o3) = {}
let o1, o2, o3 be object of (DiscrCat A); ::_thesis: ( ( o1 <> o2 or o2 <> o3 ) implies the Comp of (DiscrCat A) . (o1,o2,o3) = {} )
assume  ( o1 <> o2 or o2 <> o3 ) ; ::_thesis: the Comp of (DiscrCat A) . (o1,o2,o3) = {}
then  ( <^o1,o2^> = {} or <^o2,o3^> = {} ) by Def18;
hence  the Comp of (DiscrCat A) . (o1,o2,o3) = {} ; ::_thesis: verum
end;

theorem Th25: :: ALTCAT_1:25
for A being non empty set
for o being object of (DiscrCat A) holds the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
proof
let A be non empty set ; ::_thesis: for o being object of (DiscrCat A) holds the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
let o be object of (DiscrCat A); ::_thesis: the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
 <^o,o^> = {(id o)} by Def20;
hence  the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o) by FUNCOP_1:def_10; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster DiscrCat A ->  non empty strict pseudo-functional associative with_units quasi-discrete pseudo-discrete ;
coherence
 ( DiscrCat A is pseudo-functional & DiscrCat A is pseudo-discrete & DiscrCat A is with_units & DiscrCat A is associative )
proof
set C = DiscrCat A;
thus  DiscrCat A is pseudo-functional ::_thesis: ( DiscrCat A is pseudo-discrete & DiscrCat A is with_units & DiscrCat A is associative )
proof
let o1, o2, o3 be object of (DiscrCat A); :: according to ALTCAT_1:def_13 ::_thesis: the Comp of (DiscrCat A) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
A1: id o1 in Funcs (o1,o1) by Th1;
percases ( ( o1 = o2 & o2 = o3 ) or o1 <> o2 or o2 <> o3 ) ;
supposeA2: ( o1 = o2 & o2 = o3 ) ; ::_thesis: the Comp of (DiscrCat A) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
then A3: <^o2,o3^> = {(id o1)} by Def20;
then A4: <^o1,o2^> c= Funcs (o1,o2) by A1, A2, ZFMISC_1:31;
thus  the Comp of (DiscrCat A) . (o1,o2,o3) = ((id o1),(id o1)) :-> (id o1) by A2, Th25
.= FuncComp ({(id o1)},{(id o1)}) by Th13
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A2, A3, A4, Th14 ; ::_thesis: verum
end;
supposeA5: ( o1 <> o2 or o2 <> o3 ) ; ::_thesis: the Comp of (DiscrCat A) . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]
then A6: ( <^o2,o3^> = {} or <^o1,o2^> = {} ) by Def18;
thus  the Comp of (DiscrCat A) . (o1,o2,o3) = {} by A5, Th24
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A6 ; ::_thesis: verum
end;
end;
end;
thus  DiscrCat A is pseudo-discrete ::_thesis: ( DiscrCat A is with_units & DiscrCat A is associative )
proof
let i be object of (DiscrCat A); :: according to ALTCAT_1:def_19 ::_thesis: <^i,i^> is trivial
 <^i,i^> = {(id i)} by Def20;
hence  <^i,i^> is trivial ; ::_thesis: verum
end;
thus  DiscrCat A is with_units ::_thesis: DiscrCat A is associative
proof
thus  the Comp of (DiscrCat A) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (DiscrCat A) is with_right_units
proof
let j be Element of (DiscrCat A); :: according to ALTCAT_1:def_7 ::_thesis: ex e being set st
( e in the Arrows of (DiscrCat A) . (j,j) & ( for i being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . (e,f) = f ) )
reconsider j9 = j as object of (DiscrCat A) ;
take  id j9 ; ::_thesis: ( id j9 in the Arrows of (DiscrCat A) . (j,j) & ( for i being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f ) )
the Arrows of (DiscrCat A) . (j,j) = <^j9,j9^>
.= {(id j9)} by Def20 ;
hence  id j9 in the Arrows of (DiscrCat A) . (j,j) by TARSKI:def_1; ::_thesis: for i being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f
let i be Element of (DiscrCat A); ::_thesis: for f being set st f in the Arrows of (DiscrCat A) . (i,j) holds
( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f
let f be set ; ::_thesis: ( f in the Arrows of (DiscrCat A) . (i,j) implies ( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f )
assume A7: f in the Arrows of (DiscrCat A) . (i,j) ; ::_thesis: ( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = f
reconsider i9 = i as object of (DiscrCat A) ;
A8: the Arrows of (DiscrCat A) . (i,j) = <^i9,j9^> ;
then A9: i9 = j9 by A7, Def18;
then  f in {(id i9)} by A7, A8, Def20;
then A10: f = id i9 by TARSKI:def_1;
thus ( the Comp of (DiscrCat A) . (i,j,j)) . ((id j9),f) = (((id i9),(id i9)) :-> (id i9)) . ((id j9),f) by A9, Th25
.= f by A9, A10, Th10 ; ::_thesis: verum
end;
let j be Element of (DiscrCat A); :: according to ALTCAT_1:def_6 ::_thesis: ex e being set st
( e in the Arrows of (DiscrCat A) . (j,j) & ( for j being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (j,j) holds
( the Comp of (DiscrCat A) . (j,j,j)) . (f,e) = f ) )
reconsider j9 = j as object of (DiscrCat A) ;
take  id j9 ; ::_thesis: ( id j9 in the Arrows of (DiscrCat A) . (j,j) & ( for j being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (j,j) holds
( the Comp of (DiscrCat A) . (j,j,j)) . (f,(id j9)) = f ) )
the Arrows of (DiscrCat A) . (j,j) = <^j9,j9^>
.= {(id j9)} by Def20 ;
hence  id j9 in the Arrows of (DiscrCat A) . (j,j) by TARSKI:def_1; ::_thesis: for j being Element of the carrier of (DiscrCat A)
for f being set st f in the Arrows of (DiscrCat A) . (j,j) holds
( the Comp of (DiscrCat A) . (j,j,j)) . (f,(id j9)) = f
let i be Element of (DiscrCat A); ::_thesis: for f being set st f in the Arrows of (DiscrCat A) . (j,i) holds
( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = f
let f be set ; ::_thesis: ( f in the Arrows of (DiscrCat A) . (j,i) implies ( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = f )
assume A11: f in the Arrows of (DiscrCat A) . (j,i) ; ::_thesis: ( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = f
reconsider i9 = i as object of (DiscrCat A) ;
A12: the Arrows of (DiscrCat A) . (j,i) = <^j9,i9^> ;
then A13: i9 = j9 by A11, Def18;
then  f in {(id i9)} by A11, A12, Def20;
then A14: f = id i9 by TARSKI:def_1;
thus ( the Comp of (DiscrCat A) . (j,j,i)) . (f,(id j9)) = (((id i9),(id i9)) :-> (id i9)) . (f,(id j9)) by A13, Th25
.= f by A13, A14, Th10 ; ::_thesis: verum
end;
thus  DiscrCat A is associative ::_thesis: verum
proof
let i, j, k, l be Element of (DiscrCat A); :: according to ALTCAT_1:def_5,ALTCAT_1:def_15 ::_thesis: for f, g, h being set st f in the Arrows of (DiscrCat A) . (i,j) & g in the Arrows of (DiscrCat A) . (j,k) & h in the Arrows of (DiscrCat A) . (k,l) holds
( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f)
set G = the Arrows of (DiscrCat A);
set c = the Comp of (DiscrCat A);
reconsider i9 = i, j9 = j, k9 = k, l9 = l as object of (DiscrCat A) ;
let f, g, h be set ; ::_thesis: ( f in the Arrows of (DiscrCat A) . (i,j) & g in the Arrows of (DiscrCat A) . (j,k) & h in the Arrows of (DiscrCat A) . (k,l) implies ( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f) )
assume that
A15: f in the Arrows of (DiscrCat A) . (i,j) and
A16: g in the Arrows of (DiscrCat A) . (j,k) and
A17: h in the Arrows of (DiscrCat A) . (k,l) ; ::_thesis: ( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f)
 f in <^i9,j9^> by A15;
then A18: i9 = j9 by Def18;
A19: <^i9,i9^> = {(id i9)} by Def20;
then A20: f = id i9 by A15, A18, TARSKI:def_1;
 g in <^j9,k9^> by A16;
then A21: j9 = k9 by Def18;
then A22: g = id i9 by A16, A18, A19, TARSKI:def_1;
A23: the Comp of (DiscrCat A) . (i9,i9,i9) = ((id i9),(id i9)) :-> (id i9) by Th25;
 h in <^k9,l9^> by A17;
then A24: k9 = l9 by Def18;
then  h = id i9 by A17, A18, A21, A19, TARSKI:def_1;
hence  ( the Comp of (DiscrCat A) . (i,k,l)) . (h,(( the Comp of (DiscrCat A) . (i,j,k)) . (g,f))) = ( the Comp of (DiscrCat A) . (i,j,l)) . ((( the Comp of (DiscrCat A) . (j,k,l)) . (h,g)),f) by A18, A21, A24, A20, A22, A23, Th10; ::_thesis: verum
end;
end;
end;