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