for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by SERIES_1:5;