theorem RSI: :: RVSUM_4:61

for f being complex-valued XFinSequence holds Sum f = (Sum (Re f)) + (<i> * (Sum (Im f)))