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