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 )

( 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

( 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 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 ) 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;( 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

( 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