for seq being Complex_Sequence
for n, m being Nat holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|