theorem :: RVSUM_4:23

for seq being Complex_Sequence holds seq = (Re seq) + (<i> (#) (Im seq)) ;