let A, B be non empty transitive AltCatStr ; :: thesis:

hereby :: thesis:

assume A1: A,B have_the_same_composition ; :: thesis:
let a1, a2, a3 be Object of A; :: thesis:
assume A2: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) ; :: thesis:
let b1, b2, b3 be Object of B; :: thesis:
assume that
A3: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} ) and
A4: ( b1 = a1 & b2 = a2 & b3 = a3 ) ; :: thesis:
let f1 be Morphism of a1,a2; :: thesis:
let g1 be Morphism of b1,b2; :: thesis:
assume A5: g1 = f1 ; :: thesis:
let f2 be Morphism of a2,a3; :: thesis:
let g2 be Morphism of b2,b3; :: thesis:
assume A6: g2 = f2 ; :: thesis:
<^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:

end;

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 ; :: thesis:
let a1, a2, a3, x be object ; :: according to PARTFUN1:def 4,YELLOW20:def 1 :: thesis:
assume A11: x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) ; :: thesis:
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: