theorem XSS: :: RVSUM_4:64

for f being complex-valued XFinSequence holds Sum (XFS2FS f) = Sum f