consider n being Nat such that
A1: dom S = Seg n by FINSEQ_1:def 2;
dom (Im S) = Seg n by A1, MESFUN6C:def 2;
then A2: Im S is FinSequence by FINSEQ_1:def 2;
rng (Im S) c= REAL ;
hence Im S is FinSequence of REAL by FINSEQ_1:def 4, A2; :: thesis: verum