let F be real-valued FinSequence; :: thesis: F is FinSequence of REAL
thus rng F c= REAL ; :: according to FINSEQ_1:def 4 :: thesis: verum