let f be rational-valued FinSequence; :: thesis: f is FinSequence of RAT
thus rng f c= RAT by VALUED_0:def 4; :: according to FINSEQ_1:def 4 :: thesis: verum