consider x being Function such that
A1: ( x = f & dom x = Seg n & rng x c= Seg (n + 1) ) by FUNCT_2:def 2;
reconsider x = x as FinSequence of Seg (n + 1) by A1, FINSEQ_2:28;
Seg (n + 1) c= REAL by XBOOLE_1:1;
then x is FinSequence of REAL by FINSEQ_2:27;
hence f is FinSequence of REAL by A1; :: thesis: verum