let seq1 be Real_Sequence; :: thesis: for n, m being Nat st n <= m & ( for i being Nat holds seq1 . i >= 0 ) holds
(Partial_Sums seq1) . n <= (Partial_Sums seq1) . m
let n, m be Nat; :: thesis: ( n <= m & ( for i being Nat holds seq1 . i >= 0 ) implies (Partial_Sums seq1) . n <= (Partial_Sums seq1) . m )
assume that
A1: n <= m and
A2: for i being Nat holds seq1 . i >= 0 ; :: thesis: (Partial_Sums seq1) . n <= (Partial_Sums seq1) . m
set S = Partial_Sums seq1;
defpred S₁[ Nat] means (Partial_Sums seq1) . n <= (Partial_Sums seq1) . (n + $1);
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
set ni = n + i;
( (Partial_Sums seq1) . ((n + i) + 1) = ((Partial_Sums seq1) . (n + i)) + (seq1 . ((n + i) + 1)) & seq1 . ((n + i) + 1) >= 0 ) by A2, SERIES_1:def 1;
then (Partial_Sums seq1) . ((n + i) + 1) >= ((Partial_Sums seq1) . (n + i)) + 0 by XREAL_1:6;
hence S₁[i + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

A5: S₁[ 0 ] ;
A6: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A3);
reconsider m9 = m, n9 = n as Nat ;
A7: n9 + (m9 - n9) = m9 ;
m9 - n9 is Nat by A1, NAT_1:21;
hence (Partial_Sums seq1) . n <= (Partial_Sums seq1) . m by A6, A7; :: thesis: verum