let S1, S2 be 1-sorted ; :: thesis: Carrier <*S1,S2*> = <* the carrier of S1, the carrier of S2*>
thus Carrier <*S1,S2*> = Carrier (<*S1*> ^ <*S2*>) by FINSEQ_1:def 9
.= (Carrier <*S1*>) ^ (Carrier <*S2*>) by Th14
.= <* the carrier of S1*> ^ (Carrier <*S2*>) by Th16
.= <* the carrier of S1*> ^ <* the carrier of S2*> by Th16
.= <* the carrier of S1, the carrier of S2*> by FINSEQ_1:def 9 ; :: thesis: verum