for f being real-valued FinSequence holds f is FinSequence of REAL by RVSUM_1:145;