theorem :: RVSUM_1:145

for F being real-valued FinSequence holds F is FinSequence of REAL