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