theorem :: FINSEQ_2:134

for A being set
for i being Nat holds i -tuples_on A c= A *