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^>

the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B by A1, Def3;

then A2: [: 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:100;

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 A3: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; :: thesis: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>

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

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^>

the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B by A1, Def3;

then A2: [: 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:100;

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 A3: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; :: thesis: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>

A4: now :: thesis: ( the carrier of A <> {} & the carrier of B <> {} implies [o1,o2] in [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] )

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:] )
by PARTFUN1:def 2;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 A3, A2, XBOOLE_0:def 4; :: thesis: verum

end;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 A3, A2, XBOOLE_0:def 4; :: thesis: verum

A6: now :: thesis: ( ( the carrier of A = {} or the carrier of B = {} ) implies ( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} ) )

the Arrows of (Intersect (A,B)) = Intersect ( the Arrows of A, the Arrows of B)
by A1, Def3;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 A7: ( [: the carrier of A, the carrier of A:] = {} or [: the carrier of B, the carrier of B:] = {} ) by ZFMISC_1:90;

then ( the Arrows of A . [a1,a2] = {} or the Arrows of B . [b1,b2] = {} ) ;

hence ( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} ) by A2, A7; :: thesis: verum

end;then A7: ( [: the carrier of A, the carrier of A:] = {} or [: the carrier of B, the carrier of B:] = {} ) by ZFMISC_1:90;

then ( the Arrows of A . [a1,a2] = {} or the Arrows of B . [b1,b2] = {} ) ;

hence ( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} ) by A2, A7; :: thesis: verum

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