theorem Th17: :: PRALG_1:18

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