let rseq be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) implies ( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) )
assume A1: for n being Element of NAT holds 0 <= rseq . n ; :: thesis: ( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) )
then A2: Partial_Sums rseq is non-decreasing by SERIES_1:19;

A3: now

let n, m be Element of NAT ; :: thesis: ( n <= m implies abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) )
assume n <= m ; :: thesis: abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)
then (Partial_Sums rseq) . n <= (Partial_Sums rseq) . m by A2, SEQM_3:12;
then ((Partial_Sums rseq) . n) - ((Partial_Sums rseq) . n) <= ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by XREAL_1:11;
hence abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by ABSVALUE:def 1; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n
A4: (Partial_Sums rseq) . 0 = rseq . 0 by SERIES_1:def 1;
A5: 0 <= rseq . 0 by A1;
(Partial_Sums rseq) . 0 <= (Partial_Sums rseq) . n by A2, SEQM_3:12;
hence abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n by A4, A5, ABSVALUE:def 1; :: thesis: verum

end;

hence ( ( for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) by A3; :: thesis: verum