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