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