let D be non empty set ; :: thesis: for i being natural Number
for T being Tuple of i,D holds T is Function of (Seg i),D
let i be natural Number ; :: 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 CARD_1:def 7;
then Seg i = dom T by FINSEQ_1:def 3;
hence T is Function of (Seg i),D by FINSEQ_2:26; :: thesis: verum