theorem RSF: :: RVSUM_4:24

for f being complex-valued XFinSequence holds Re (Sequel f) = Sequel (Re f)