set Cr = the carrier of A /\ the carrier of B;
A2: [:(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:] by ZFMISC_1:123;
consider Ar being ManySortedSet of such that
A3: Ar = Intersect the Arrows of A,the Arrows of B and
A4: Intersect {|the Arrows of A|},{|the Arrows of B|} = {|Ar|} by Th18;
consider Ar1, Ar2 being ManySortedSet of such that
A5: ( Ar1 = Intersect the Arrows of A,the Arrows of B & Ar2 = Intersect the Arrows of A,the Arrows of B ) and
A6: Intersect {|the Arrows of A,the Arrows of A|},{|the Arrows of B,the Arrows of B|} = {|Ar1,Ar2|} by Th19;
( [:the carrier of A,the carrier of A,the carrier of A:] = [:[: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 B,the carrier of B:],the carrier of B:] ) by ZFMISC_1:def 3;
then A7: [: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 A2, 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 ;
A8: ( dom the Comp of A = [:the carrier of A,the carrier of A,the carrier of A:] & dom the Comp of B = [:the carrier of B,the carrier of B,the carrier of B:] ) by PARTFUN1:def 4;

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 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 )
then consider a1, a2, a3 being set such that
( a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A ) and
A9: x = [a1,a2,a3] by A8, MCART_1:72;
assume x in dom the Comp of B ; :: thesis: the Comp of A . x tolerates the Comp of B . x
thus the Comp of A . x tolerates the Comp of B . x by A1, A9, Def1; :: thesis: verum

end;

then reconsider Cm = Intersect the Comp of A,the Comp of B as ManySortedFunction of {|Ar,Ar|},{|Ar|} by A3, A4, A5, A6, A7, 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 A3; :: thesis: verum