for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
for m being Nat holds (Partial_Sums |.seq.|) . m = 0