let A, B be AltCatStr ; :: thesis: ( A,B have_the_same_composition implies for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect A,B) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> )
assume A1: A,B have_the_same_composition ; :: thesis: for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect A,B) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let a1, a2 be object of A; :: thesis: for b1, b2 being object of B
for o1, o2 being object of (Intersect A,B) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let b1, b2 be object of B; :: thesis: for o1, o2 being object of (Intersect A,B) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let o1, o2 be object of (Intersect A,B); :: thesis: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 implies <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> )
assume A2: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; :: thesis: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
A3: ( the carrier of (Intersect A,B) = the carrier of A /\ the carrier of B & the Arrows of (Intersect A,B) = Intersect the Arrows of A,the Arrows of B ) by A1, Def3;
then A4: [:the carrier of (Intersect A,B),the carrier of (Intersect A,B):] = [:the carrier of A,the carrier of A:] /\ [:the carrier of B,the carrier of B:] by ZFMISC_1:123;
A5: ( dom the Arrows of A = [:the carrier of A,the carrier of A:] & dom the Arrows of B = [:the carrier of B,the carrier of B:] & dom the Arrows of (Intersect A,B) = [:the carrier of (Intersect A,B),the carrier of (Intersect A,B):] ) by PARTFUN1:def 4;

A6: now

assume ( the carrier of A <> {} & the carrier of B <> {} ) ; :: thesis: [o1,o2] in [:the carrier of (Intersect A,B),the carrier of (Intersect A,B):]
then ( [a1,a2] in [:the carrier of A,the carrier of A:] & [b1,b2] in [:the carrier of B,the carrier of B:] ) by ZFMISC_1:def 2;
hence [o1,o2] in [:the carrier of (Intersect A,B),the carrier of (Intersect A,B):] by A2, A4, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume ( the carrier of A = {} or the carrier of B = {} ) ; :: thesis: ( (the Arrows of A . [a1,a2]) /\ (the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect A,B) . [o1,o2] = {} )
then ( [:the carrier of A,the carrier of A:] = {} or [:the carrier of B,the carrier of B:] = {} ) by ZFMISC_1:113;
then ( [:the carrier of (Intersect A,B),the carrier of (Intersect A,B):] = {} & ( the Arrows of A . [a1,a2] = {} or the Arrows of B . [b1,b2] = {} ) ) by A4, A5, FUNCT_1:def 4;
hence ( (the Arrows of A . [a1,a2]) /\ (the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect A,B) . [o1,o2] = {} ) by A5, FUNCT_1:def 4; :: thesis: verum

end;

hence <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A2, A3, A4, A5, A6, Def2; :: thesis: verum