for s being Real_Sequence
for n, m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums |.s.|) . m) - ((Partial_Sums |.s.|) . n)).|