let s be Real_Sequence; :: thesis: 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)).|
let n, m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums |.s.|) . m) - ((Partial_Sums |.s.|) . n)).| )
assume A1: n <= m ; :: thesis: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums |.s.|) . m) - ((Partial_Sums |.s.|) . n)).|
reconsider u = n, v = m as Integer ;
set s2 = Partial_Sums (abs s);
set s1 = Partial_Sums s;
defpred S₁[ Nat] means |.(((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums (abs s)) . (n + $1)) - ((Partial_Sums (abs s)) . n)).|;

now :: thesis: for k being Nat holds (abs s) . k >= 0

let k be Nat; :: thesis: (abs s) . k >= 0
|.(s . k).| >= 0 by COMPLEX1:46;
hence (abs s) . k >= 0 by SEQ_1:12; :: thesis: verum

end;

then A2: Partial_Sums (abs s) is non-decreasing by Th16;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: |.(s . ((n + k) + 1)).| >= 0 by COMPLEX1:46;
assume |.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)).| ; :: thesis: S₁[k + 1]
then A5: |.(s . ((n + k) + 1)).| + |.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).| <= |.(s . ((n + k) + 1)).| + |.(((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)).| by XREAL_1:7;
A6: |.(((Partial_Sums (abs s)) . (n + (k + 1))) - ((Partial_Sums (abs s)) . n)).| = |.((((Partial_Sums (abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) - ((Partial_Sums (abs s)) . n)).| by Def1
.= |.((|.(s . ((n + k) + 1)).| + ((Partial_Sums (abs s)) . (n + k))) - ((Partial_Sums (abs s)) . n)).| by SEQ_1:12
.= |.(|.(s . ((n + k) + 1)).| + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))).| ;
(Partial_Sums (abs s)) . (n + k) >= (Partial_Sums (abs s)) . n by A2, SEQM_3:5;
then A7: ((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n) >= 0 by XREAL_1:48;
|.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).| = |.(((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)).| by Def1
.= |.((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))).| ;
then |.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).| <= |.(s . ((n + k) + 1)).| + |.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).| by COMPLEX1:56;
then |.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).| <= |.(s . ((n + k) + 1)).| + |.(((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)).| by A5, XXREAL_0:2;
then |.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).| <= |.(s . ((n + k) + 1)).| + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) by A7, ABSVALUE:def 1;
hence S₁[k + 1] by A7, A4, A6, ABSVALUE:def 1; :: thesis: verum

end;

reconsider k = v - u as Element of NAT by A1, INT_1:5;
A8: n + k = m ;
A9: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A3);
hence |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums |.s.|) . m) - ((Partial_Sums |.s.|) . n)).| by A8; :: thesis: verum