let i be natural Number ; :: 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 12;
dom f = Seg i by FUNCT_2:def 1;
then A1: f is FinSequence by FINSEQ_1:def 2;
rng f c= D by RELAT_1:def 19;
hence f is FinSequence of D by A1, FINSEQ_1:def 4; :: thesis: verum