let A, B be non empty transitive AltCatStr ; :: thesis: ( A,B have_the_same_composition iff for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 ; :: thesis: A,B have_the_same_composition

let a1, a2, a3, x be object ; :: according to PARTFUN1:def 4,YELLOW20:def 1 :: thesis: ( not x in (proj1 ( the Comp of A . [a1,a2,a3])) /\ (proj1 ( the Comp of B . [a1,a2,a3])) or ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )

assume A11: x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) ; :: thesis: ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x

then A12: x in dom ( the Comp of A . [a1,a2,a3]) by XBOOLE_0:def 4;

then [a1,a2,a3] in dom the Comp of A by FUNCT_1:def 2, RELAT_1:38;

then A13: [a1,a2,a3] in [: the carrier of A, the carrier of A, the carrier of A:] ;

A14: x in dom ( the Comp of B . [a1,a2,a3]) by A11, XBOOLE_0:def 4;

then [a1,a2,a3] in dom the Comp of B by FUNCT_1:def 2, RELAT_1:38;

then A15: [a1,a2,a3] in [: the carrier of B, the carrier of B, the carrier of B:] ;

reconsider a1 = a1, a2 = a2, a3 = a3 as Object of A by A13, MCART_1:69;

reconsider b1 = a1, b2 = a2, b3 = a3 as Object of B by A15, MCART_1:69;

A16: the Comp of A . (a1,a2,a3) = the Comp of A . [a1,a2,a3] by MULTOP_1:def 1;

then ( [:<^a2,a3^>,<^a1,a2^>:] <> {} implies <^a1,a3^> <> {} ) by A11, XBOOLE_0:def 4;

then dom ( the Comp of A . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by FUNCT_2:def 1;

then consider f2, f1 being object such that

A17: f2 in <^a2,a3^> and

A18: f1 in <^a1,a2^> and

A19: x = [f2,f1] by A12, A16, ZFMISC_1:def 2;

reconsider f1 = f1 as Morphism of a1,a2 by A18;

reconsider f2 = f2 as Morphism of a2,a3 by A17;

A20: the Comp of B . (b1,b2,b3) = the Comp of B . [b1,b2,b3] by MULTOP_1:def 1;

then ( [:<^b2,b3^>,<^b1,b2^>:] <> {} implies <^b1,b3^> <> {} ) by A11, XBOOLE_0:def 4;

then A21: dom ( the Comp of B . (b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by FUNCT_2:def 1;

then A22: ( f1 in <^b1,b2^> & f2 in <^b2,b3^> ) by A14, A20, A19, ZFMISC_1:87;

reconsider g2 = f2 as Morphism of b2,b3 by A14, A20, A21, A19, ZFMISC_1:87;

reconsider g1 = f1 as Morphism of b1,b2 by A14, A20, A21, A19, ZFMISC_1:87;

( the Comp of A . [a1,a2,a3]) . x = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by A19, MULTOP_1:def 1

.= f2 * f1 by A17, A18, ALTCAT_1:def 8

.= g2 * g1 by A10, A17, A18, A22

.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A22, ALTCAT_1:def 8 ;

hence ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A19, MULTOP_1:def 1; :: thesis: verum

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

hereby :: thesis: ( ( for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 ) implies A,B have_the_same_composition )

assume A10:
for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 ) implies A,B have_the_same_composition )

assume A1:
A,B have_the_same_composition
; :: thesis: for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let a1, a2, a3 be Object of A; :: thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} implies for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

assume A2: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) ; :: thesis: for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let b1, b2, b3 be Object of B; :: thesis: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 implies for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

assume that

A3: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} ) and

A4: ( b1 = a1 & b2 = a2 & b3 = a3 ) ; :: thesis: for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let f1 be Morphism of a1,a2; :: thesis: for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let g1 be Morphism of b1,b2; :: thesis: ( g1 = f1 implies for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

assume A5: g1 = f1 ; :: thesis: for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let f2 be Morphism of a2,a3; :: thesis: for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let g2 be Morphism of b2,b3; :: thesis: ( g2 = f2 implies f2 * f1 = g2 * g1 )

assume A6: g2 = f2 ; :: thesis: f2 * f1 = g2 * g1

<^b1,b3^> <> {} by A3, ALTCAT_1:def 2;

then dom ( the Comp of B . (b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by FUNCT_2:def 1;

then A7: [g2,g1] in dom ( the Comp of B . (b1,b2,b3)) by A3, ZFMISC_1:def 2;

<^a1,a3^> <> {} by A2, ALTCAT_1:def 2;

then dom ( the Comp of A . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by FUNCT_2:def 1;

then A8: [f2,f1] in dom ( the Comp of A . (a1,a2,a3)) by A2, ZFMISC_1:def 2;

A9: ( the Comp of A . (a1,a2,a3) = the Comp of A . [a1,a2,a3] & the Comp of B . (b1,b2,b3) = the Comp of B . [b1,b2,b3] ) by MULTOP_1:def 1;

thus f2 * f1 = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by A2, ALTCAT_1:def 8

.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A1, A4, A5, A6, A9, A8, A7, Th10

.= g2 * g1 by A3, ALTCAT_1:def 8 ; :: thesis: verum

end;for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let a1, a2, a3 be Object of A; :: thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} implies for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

assume A2: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) ; :: thesis: for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let b1, b2, b3 be Object of B; :: thesis: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 implies for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

assume that

A3: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} ) and

A4: ( b1 = a1 & b2 = a2 & b3 = a3 ) ; :: thesis: for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let f1 be Morphism of a1,a2; :: thesis: for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let g1 be Morphism of b1,b2; :: thesis: ( g1 = f1 implies for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 )

assume A5: g1 = f1 ; :: thesis: for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let f2 be Morphism of a2,a3; :: thesis: for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1

let g2 be Morphism of b2,b3; :: thesis: ( g2 = f2 implies f2 * f1 = g2 * g1 )

assume A6: g2 = f2 ; :: thesis: f2 * f1 = g2 * g1

<^b1,b3^> <> {} by A3, ALTCAT_1:def 2;

then dom ( the Comp of B . (b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by FUNCT_2:def 1;

then A7: [g2,g1] in dom ( the Comp of B . (b1,b2,b3)) by A3, ZFMISC_1:def 2;

<^a1,a3^> <> {} by A2, ALTCAT_1:def 2;

then dom ( the Comp of A . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by FUNCT_2:def 1;

then A8: [f2,f1] in dom ( the Comp of A . (a1,a2,a3)) by A2, ZFMISC_1:def 2;

A9: ( the Comp of A . (a1,a2,a3) = the Comp of A . [a1,a2,a3] & the Comp of B . (b1,b2,b3) = the Comp of B . [b1,b2,b3] ) by MULTOP_1:def 1;

thus f2 * f1 = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by A2, ALTCAT_1:def 8

.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A1, A4, A5, A6, A9, A8, A7, Th10

.= g2 * g1 by A3, ALTCAT_1:def 8 ; :: thesis: verum

for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds

for f1 being Morphism of a1,a2

for g1 being Morphism of b1,b2 st g1 = f1 holds

for f2 being Morphism of a2,a3

for g2 being Morphism of b2,b3 st g2 = f2 holds

f2 * f1 = g2 * g1 ; :: thesis: A,B have_the_same_composition

let a1, a2, a3, x be object ; :: according to PARTFUN1:def 4,YELLOW20:def 1 :: thesis: ( not x in (proj1 ( the Comp of A . [a1,a2,a3])) /\ (proj1 ( the Comp of B . [a1,a2,a3])) or ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )

assume A11: x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) ; :: thesis: ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x

then A12: x in dom ( the Comp of A . [a1,a2,a3]) by XBOOLE_0:def 4;

then [a1,a2,a3] in dom the Comp of A by FUNCT_1:def 2, RELAT_1:38;

then A13: [a1,a2,a3] in [: the carrier of A, the carrier of A, the carrier of A:] ;

A14: x in dom ( the Comp of B . [a1,a2,a3]) by A11, XBOOLE_0:def 4;

then [a1,a2,a3] in dom the Comp of B by FUNCT_1:def 2, RELAT_1:38;

then A15: [a1,a2,a3] in [: the carrier of B, the carrier of B, the carrier of B:] ;

reconsider a1 = a1, a2 = a2, a3 = a3 as Object of A by A13, MCART_1:69;

reconsider b1 = a1, b2 = a2, b3 = a3 as Object of B by A15, MCART_1:69;

A16: the Comp of A . (a1,a2,a3) = the Comp of A . [a1,a2,a3] by MULTOP_1:def 1;

then ( [:<^a2,a3^>,<^a1,a2^>:] <> {} implies <^a1,a3^> <> {} ) by A11, XBOOLE_0:def 4;

then dom ( the Comp of A . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by FUNCT_2:def 1;

then consider f2, f1 being object such that

A17: f2 in <^a2,a3^> and

A18: f1 in <^a1,a2^> and

A19: x = [f2,f1] by A12, A16, ZFMISC_1:def 2;

reconsider f1 = f1 as Morphism of a1,a2 by A18;

reconsider f2 = f2 as Morphism of a2,a3 by A17;

A20: the Comp of B . (b1,b2,b3) = the Comp of B . [b1,b2,b3] by MULTOP_1:def 1;

then ( [:<^b2,b3^>,<^b1,b2^>:] <> {} implies <^b1,b3^> <> {} ) by A11, XBOOLE_0:def 4;

then A21: dom ( the Comp of B . (b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by FUNCT_2:def 1;

then A22: ( f1 in <^b1,b2^> & f2 in <^b2,b3^> ) by A14, A20, A19, ZFMISC_1:87;

reconsider g2 = f2 as Morphism of b2,b3 by A14, A20, A21, A19, ZFMISC_1:87;

reconsider g1 = f1 as Morphism of b1,b2 by A14, A20, A21, A19, ZFMISC_1:87;

( the Comp of A . [a1,a2,a3]) . x = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by A19, MULTOP_1:def 1

.= f2 * f1 by A17, A18, ALTCAT_1:def 8

.= g2 * g1 by A10, A17, A18, A22

.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A22, ALTCAT_1:def 8 ;

hence ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A19, MULTOP_1:def 1; :: thesis: verum