let f be INT -valued FinSequence; :: thesis: f is FinSequence of REAL
rng f c= REAL ;
hence f is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum