let i be natural Number ; :: thesis: for D being non empty set
for d being Element of D holds i |-> d is Element of i -tuples_on D
let D be non empty set ; :: thesis: for d being Element of D holds i |-> d is Element of i -tuples_on D
let d be Element of D; :: thesis: i |-> d is Element of i -tuples_on D
( i |-> d is FinSequence of D & len (i |-> d) = i ) by Th61, CARD_1:def 7;
hence i |-> d is Element of i -tuples_on D by Lm6; :: thesis: verum