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