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

rng f c= REAL ;

hence f is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum