theorem XSF: :: RVSUM_4:60

for f being XFinSequence of REAL holds Sum (XFS2FS f) = Sum f