A2: now :: thesis: for x being set st x in dom the Comp of A & x in dom the Comp of B holds

the Comp of A . x tolerates the Comp of B . x

set Cr = the carrier of A /\ the carrier of B;the Comp of A . x tolerates the Comp of B . x

let x be set ; :: thesis: ( x in dom the Comp of A & x in dom the Comp of B implies the Comp of A . x tolerates the Comp of B . x )

assume A3: x in dom the Comp of A ; :: thesis: ( x in dom the Comp of B implies the Comp of A . x tolerates the Comp of B . x )

assume x in dom the Comp of B ; :: thesis: the Comp of A . x tolerates the Comp of B . x

ex a1, a2, a3 being object st

( a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & x = [a1,a2,a3] ) by A3, MCART_1:68;

hence the Comp of A . x tolerates the Comp of B . x by A1; :: thesis: verum

end;assume A3: x in dom the Comp of A ; :: thesis: ( x in dom the Comp of B implies the Comp of A . x tolerates the Comp of B . x )

assume x in dom the Comp of B ; :: thesis: the Comp of A . x tolerates the Comp of B . x

ex a1, a2, a3 being object st

( a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & x = [a1,a2,a3] ) by A3, MCART_1:68;

hence the Comp of A . x tolerates the Comp of B . x by A1; :: thesis: verum

A4: [: the carrier of B, the carrier of B, the carrier of B:] = [:[: the carrier of B, the carrier of B:], the carrier of B:] by ZFMISC_1:def 3;

( [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] = [: the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B:] & [: the carrier of A, the carrier of A, the carrier of A:] = [:[: the carrier of A, the carrier of A:], the carrier of A:] ) by ZFMISC_1:100, ZFMISC_1:def 3;

then A5: [: the carrier of A, the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B, the carrier of B:] = [:[:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):],( the carrier of A /\ the carrier of B):] by A4, ZFMISC_1:100

.= [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] by ZFMISC_1:def 3 ;

consider Ar being ManySortedSet of [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] such that

A6: Ar = Intersect ( the Arrows of A, the Arrows of B) and

A7: Intersect ({| the Arrows of A|},{| the Arrows of B|}) = {|Ar|} by Th17;

ex Ar1, Ar2 being ManySortedSet of [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] st

( Ar1 = Intersect ( the Arrows of A, the Arrows of B) & Ar2 = Intersect ( the Arrows of A, the Arrows of B) & Intersect ({| the Arrows of A, the Arrows of A|},{| the Arrows of B, the Arrows of B|}) = {|Ar1,Ar2|} ) by Th18;

then reconsider Cm = Intersect ( the Comp of A, the Comp of B) as ManySortedFunction of {|Ar,Ar|},{|Ar|} by A6, A7, A5, A2, Th16;

take AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) ; :: thesis: ( the carrier of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = the carrier of A /\ the carrier of B & the Arrows of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Arrows of A, the Arrows of B) & the Comp of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Comp of A, the Comp of B) )

thus ( the carrier of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = the carrier of A /\ the carrier of B & the Arrows of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Arrows of A, the Arrows of B) & the Comp of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Comp of A, the Comp of B) ) by A6; :: thesis: verum