let i be Nat; :: thesis: for D being non empty set
for f being Function of Seg i,D holds f is FinSequence of D
let D be non empty set ; :: thesis: for f being Function of Seg i,D holds f is FinSequence of D
let f be Function of Seg i,D; :: thesis: f is FinSequence of D
reconsider i = i as Element of NAT by ORDINAL1:def 13;
dom f = Seg i by FUNCT_2:def 1;
then ( f is FinSequence & rng f c= D ) by FINSEQ_1:def 2, RELSET_1:12;
hence f is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum