let seq1 be Real_Sequence; :: thesis: for n, m being Element of NAT st n <= m & ( for i being Element of NAT holds seq1 . i >= 0 ) holds
(Partial_Sums seq1) . n <= (Partial_Sums seq1) . m
let n, m be Element of NAT ; :: thesis: ( n <= m & ( for i being Element of NAT holds seq1 . i >= 0 ) implies (Partial_Sums seq1) . n <= (Partial_Sums seq1) . m )
assume that
A1: n <= m and
A2: for i being Element of 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: S₁[ 0 ] ;
A4: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: 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:8;
hence S₁[i + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

A6: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A3, A4);
reconsider m' = m, n' = n as Nat ;
A7: m' - n' is Element of NAT by A1, NAT_1:21;
n' + (m' - n') = m' ;
hence (Partial_Sums seq1) . n <= (Partial_Sums seq1) . m by A6, A7; :: thesis: verum