for n being Nat
for X being set holds product ((Seg n) --> X) = n -tuples_on X