theorem :: CLASSES4:60
for UN being Universe
for X being set st X in UN holds
for n being Nat holds n -tuples_on X in UN