let f be complex-valued XFinSequence; :: thesis: Sum f = (Sum (Re f)) + (<i> * (Sum (Im f)))
reconsider g = Re f as len f -element real-valued XFinSequence ;
len (<i> (#) (Im f)) = dom (Im f) by VALUED_1:def 5
.= len f by CARD_1:def 7 ;
then reconsider h = <i> (#) (Im f) as len f -element complex-valued XFinSequence by CARD_1:def 7;
Sum f = Sum ((Re f) + (<i> (#) (Im f)))
.= (Sum g) + (Sum h) by SPP
.= (Sum (Re f)) + (<i> * (Sum (Im f))) by AFINSQ_2:64 ;
hence Sum f = (Sum (Re f)) + (<i> * (Sum (Im f))) ; :: thesis: verum