let A, B be AltCatStr ; :: thesis: ( A,B have_the_same_composition iff for a1, a2, a3, x being object st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )

hereby :: thesis: ( ( for a1, a2, a3, x being object st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x ) implies A,B have_the_same_composition )

assume A1: A,B have_the_same_composition ; :: thesis: for a1, a2, a3, x being object st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x
let a1, a2, a3, x be object ; :: thesis: ( x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) implies ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
assume ( x in dom ( the Comp of A . [a1,a2,a3]) & x in 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 A2: x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) by XBOOLE_0:def 4;
the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] by A1;
hence ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A2; :: thesis: verum

end;

assume A3: for a1, a2, a3, x being object st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x ; :: 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 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 ( x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) ) by XBOOLE_0:def 4;
hence ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A3; :: thesis: verum