let A, B be AltCatStr ; ( 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 ( ( 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
;
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]) . xlet a1,
a2,
a3,
x be
object ;
( 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]) )
;
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . xthen 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;
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
; A,B have_the_same_composition
let a1, a2, a3, x be object ; PARTFUN1:def 4,YELLOW20:def 1 ( 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]))
; ( 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; verum