rng (Im S) c= REAL ;
hence Im S is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum