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
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;
set Cr = the carrier of A /\ the carrier of B;
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