for seq being Complex_Sequence
for z being Complex holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)