for seq being Complex_Sequence holds Partial_Sums (seq *') = (Partial_Sums seq) *' by Lm1;