theorem :: CLASSES4:61

for X being set
for n being Nat holds n -tuples_on X c= X * by FINSEQ_2:90;