let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= rseq . n ) implies ( ( 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 ) ) )
assume A1: for n being Nat holds 0 <= rseq . n ; :: thesis: ( ( 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 ) )
then A2: Partial_Sums rseq is non-decreasing by SERIES_1:16;
A3: now :: thesis: 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)
let n, m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)).| = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) )
assume n <= m ; :: thesis: |.(((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:6;
then ((Partial_Sums rseq) . n) - ((Partial_Sums rseq) . n) <= ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by XREAL_1:9;
hence |.(((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)).| = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by ABSVALUE:def 1; :: thesis: verum
end;
now :: thesis: for n being Nat holds |.((Partial_Sums rseq) . n).| = (Partial_Sums rseq) . n
let n be Nat; :: thesis: |.((Partial_Sums rseq) . n).| = (Partial_Sums rseq) . n
A4: (Partial_Sums rseq) . 0 <= (Partial_Sums rseq) . n by A2, SEQM_3:6;
( (Partial_Sums rseq) . 0 = rseq . 0 & 0 <= rseq . 0 ) by A1, SERIES_1:def 1;
hence |.((Partial_Sums rseq) . n).| = (Partial_Sums rseq) . n by A4, ABSVALUE:def 1; :: thesis: verum
end;
hence ( ( 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 ) ) by A3; :: thesis: verum