let D be non empty set ; :: thesis: for i being Nat
for T being Element of i -tuples_on D holds T is Function of (Seg i),D
let i be Nat; :: thesis: for T being Element of i -tuples_on D holds T is Function of (Seg i),D
let T be Element of i -tuples_on D; :: thesis: T is Function of (Seg i),D
len T = i by FINSEQ_1:def 18;
then Seg i = dom T by FINSEQ_1:def 3;
hence T is Function of (Seg i),D by FINSEQ_2:30; :: thesis: verum