let i be Nat; :: 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
A: z is Element of D * by FINSEQ_1:def 11;
len z = i by FINSEQ_1:def 18;
hence z in i -tuples_on D by A; :: thesis: verum