theorem SSF: :: RVSUM_4:66

for f being real-valued XFinSequence holds Sum f = Sum (Sequel f)