let A, B be AltCatStr ; :: thesis: ( A,B have_the_same_composition iff for a1, a2, a3, x being set 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 set 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 set 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 set ; :: 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 that
A2: x in dom (the Comp of A . [a1,a2,a3]) and
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
( x in (dom (the Comp of A . [a1,a2,a3])) /\ (dom (the Comp of B . [a1,a2,a3])) & the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] ) by A1, A2, A3, Def1, XBOOLE_0:def 4;
hence (the Comp of A . [a1,a2,a3]) . x = (the Comp of B . [a1,a2,a3]) . x by PARTFUN1:def 6; :: thesis: verum

end;

assume A4: for a1, a2, a3, x being set 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 set ; :: according to PARTFUN1:def 6,YELLOW20:def 1 :: thesis: ( not x in (dom (the Comp of A . [a1,a2,a3])) /\ (dom (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 A4; :: thesis: verum