:: 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;