theorem :: RVSUM_4:63

for f being complex-valued XFinSequence holds
( XFS2FS (Re f) = Re (XFS2FS f) & XFS2FS (Im f) = Im (XFS2FS f) ) by RSH;