theorem Th129: :: FINSEQ_3:131

for i being Nat
for D being set holds product (i |-> D) = i -tuples_on D