for seq being Complex_Sequence
for k being Nat holds
( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) )