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))
set s1 = Partial_Sums s;
set s2 = Partial_Sums (abs 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));
A2: S₁[ 0 ] ;

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 A3: Partial_Sums (abs s) is non-decreasing by Th19;
A4: 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] )
assume A5: 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]
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 A6: 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;
(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 A5, XREAL_1:9;
then A7: 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 A6, XXREAL_0:2;
(Partial_Sums (abs s)) . (n + k) >= (Partial_Sums (abs s)) . n by A3, SEQM_3:11;
then A8: ((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n) >= 0 by XREAL_1:50;
then A9: 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;
abs (s . ((n + k) + 1)) >= 0 by COMPLEX1:132;
then A10: (abs (s . ((n + k) + 1))) + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) >= 0 + 0 by A8;
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))) ;
hence S₁[k + 1] by A9, A10, ABSVALUE:def 1; :: thesis: verum

end;

A11: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A4);
reconsider u = n, v = m as Integer ;
reconsider k = v - u as Element of NAT by A1, INT_1:18;
n + k = m ;
hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by A11; :: thesis: verum