set d = the Element of D;
i |-> the Element of D is FinSequence of D by Th61;
then reconsider S = i |-> the Element of D as Element of D * by FINSEQ_1:def 11;
len S = i by CARD_1:def 7;
then S in { s where s is Element of D * : len s = i } ;
hence not i -tuples_on D is empty ; :: thesis: verum