theorem XSF: :: RVSUM_4:60
for f being XFinSequence of REAL holds Sum (XFS2FS f) = Sum f