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

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