theorem :: PRALG_1:19

for S1, S2, S3 being 1-sorted holds Carrier <*S1,S2,S3*> = <* the carrier of S1, the carrier of S2, the carrier of S3*>