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 )

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 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 ;
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 ;
<^a1,a3^> <> {} by ;
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 ;
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
.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A1, A4, A5, A6, A9, A8, A7, Th10
.= g2 * g1 by ; :: thesis: verum
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: ( 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 ;
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 ;
then [a1,a2,a3] in dom the Comp of B by ;
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 ;
reconsider b1 = a1, b2 = a2, b3 = a3 as Object of B by ;
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 ;
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 ;
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 ;
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 ;
reconsider g2 = f2 as Morphism of b2,b3 by ;
reconsider g1 = f1 as Morphism of b1,b2 by ;
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by
.= f2 * f1 by
.= g2 * g1 by A10, A17, A18, A22
.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by ;
hence ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by ; :: thesis: verum