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