consider d being Element of D;
i |-> d is FinSequence of D by Th77;
then reconsider S = i |-> d as Element of D * by FINSEQ_1:def 11;
len S = i by FINSEQ_1:def 18;
then S in { s where s is Element of D * : len s = i } ;
hence not i -tuples_on D is empty ; :: thesis: verum