theorem Th8: :: SRINGS_5:10

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