let i be natural Number ; :: thesis: for D being non empty set
for z being Tuple of i,D holds z in i -tuples_on D
let D be non empty set ; :: thesis: for z being Tuple of i,D holds z in i -tuples_on D
let z be Tuple of i,D; :: thesis: z in i -tuples_on D
A1: z is Element of D * by FINSEQ_1:def 11;
len z = i by CARD_1:def 7;
hence z in i -tuples_on D by A1; :: thesis: verum