let D be non empty set ; :: thesis: for i being Nat
for T being Tuple of i,D holds T is Function of (Seg i),D
let i be Nat; :: thesis: for T being Tuple of i,D holds T is Function of (Seg i),D
let T be Tuple of i,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