let s be Real_Sequence; :: thesis: for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n))
let n, m be Element of NAT ; :: thesis: ( n <= m implies abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) )
assume A1: n <= m ; :: thesis: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n))
reconsider u = n, v = m as Integer ;
set s2 = Partial_Sums (abs s);
set s1 = Partial_Sums s;
defpred S₁[ Element of NAT ] means abs (((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . (n + $1)) - ((Partial_Sums (abs s)) . n));

now

let k be Element of NAT ; :: thesis: (abs s) . k >= 0
abs (s . k) >= 0 by COMPLEX1:132;
hence (abs s) . k >= 0 by SEQ_1:16; :: thesis: verum

end;

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

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: abs (s . ((n + k) + 1)) >= 0 by COMPLEX1:132;
assume abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) ; :: thesis: S₁[k + 1]
then A5: (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) by XREAL_1:9;
A6: abs (((Partial_Sums (abs s)) . (n + (k + 1))) - ((Partial_Sums (abs s)) . n)) = abs ((((Partial_Sums (abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) - ((Partial_Sums (abs s)) . n)) by Def1
.= abs (((abs (s . ((n + k) + 1))) + ((Partial_Sums (abs s)) . (n + k))) - ((Partial_Sums (abs s)) . n)) by SEQ_1:16
.= abs ((abs (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:11;
then A7: ((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n) >= 0 by XREAL_1:50;
abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) = abs (((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)) by Def1
.= abs ((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) ;
then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) by COMPLEX1:142;
then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) by A5, XXREAL_0:2;
then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (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:18;
A8: n + k = m ;
A9: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A9, A3);
hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by A8; :: thesis: verum