reconsider h = Im f as real-valued Complex_Sequence by RSC;
Partial_Sums h is convergent by SERIES_1:def 2;
hence Im f is real-valued summable Complex_Sequence by COMSEQ_3:def 8; :: thesis: verum