theorem Th58: :: CLASSES4:58
for UN being Universe
for D being set st D in UN holds
for n being Nat holds n -tuples_on D in UN