A2: dom the Comp of A = [: the carrier of A, the carrier of A, the carrier of A:] by PARTFUN1:def 4;

A3: now

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 A4: 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 set st
( a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & x = [a1,a2,a3] ) by A2, A4, MCART_1:72;
hence the Comp of A . x tolerates the Comp of B . x by A1, Def1; :: thesis: verum

end;

set Cr = the carrier of A /\ the carrier of B;
A5: [: 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:123, ZFMISC_1:def 3;
then A6: [: 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 A5, ZFMISC_1:123
.= [:( 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
A7: Ar = Intersect ( the Arrows of A, the Arrows of B) and
A8: Intersect ({| the Arrows of A|},{| the Arrows of B|}) = {|Ar|} by Th18;
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 Th19;
then reconsider Cm = Intersect ( the Comp of A, the Comp of B) as ManySortedFunction of {|Ar,Ar|},{|Ar|} by A7, A8, A6, A3, Th17;
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 A7; :: thesis: verum