consider x being Function such that

A1: x = f and

dom x = Seg n and

rng x c= Seg (n + 1) by FUNCT_2:def 2;

reconsider x = x as FinSequence of Seg (n + 1) by A1, FINSEQ_2:25;

Seg (n + 1) c= REAL by NUMBERS:19;

then x is FinSequence of REAL by FINSEQ_2:24;

hence f is FinSequence of REAL by A1; :: thesis: verum

A1: x = f and

dom x = Seg n and

rng x c= Seg (n + 1) by FUNCT_2:def 2;

reconsider x = x as FinSequence of Seg (n + 1) by A1, FINSEQ_2:25;

Seg (n + 1) c= REAL by NUMBERS:19;

then x is FinSequence of REAL by FINSEQ_2:24;

hence f is FinSequence of REAL by A1; :: thesis: verum