:: deftheorem defines -tuples_on FINSEQ_2:def 4 :
for i being natural Number
for D being set holds i -tuples_on D = { s where s is Element of D * : len s = i } ;