theorem Th110: :: FINSEQ_2:112

for i being natural Number
for D being non empty set
for d being Element of D holds i |-> d is Element of i -tuples_on D