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