theorem ISF: :: RVSUM_4:25

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