let f, g be Real_Sequence; :: thesis: for M, N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds
f . n <= g . n ) holds
Sum (f,N,M) <= Sum (g,N,M)
let M be Element of NAT ; :: thesis: for N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds
f . n <= g . n ) holds
Sum (f,N,M) <= Sum (g,N,M)
defpred S₁[ Nat] means ( ( for n being Element of NAT st M + 1 <= n & n <= $1 holds
f . n <= g . n ) implies Sum (f,$1,M) <= Sum (g,$1,M) );
A1: for N1 being Nat st N1 >= M + 1 & S₁[N1] holds
S₁[N1 + 1]

proof

let N1 be Nat; :: thesis: ( N1 >= M + 1 & S₁[N1] implies S₁[N1 + 1] )
assume that
A2: N1 >= M + 1 and
A3: ( ( for n being Element of NAT st M + 1 <= n & n <= N1 holds
f . n <= g . n ) implies Sum (f,N1,M) <= Sum (g,N1,M) ) ; :: thesis: S₁[N1 + 1]
assume A4: for n being Element of NAT st M + 1 <= n & n <= N1 + 1 holds
f . n <= g . n ; :: thesis: Sum (f,(N1 + 1),M) <= Sum (g,(N1 + 1),M)

A5: now :: thesis: for n being Element of NAT st M + 1 <= n & n <= N1 holds
f . n <= g . n

let n be Element of NAT ; :: thesis: ( M + 1 <= n & n <= N1 implies f . n <= g . n )
assume that
A6: M + 1 <= n and
A7: n <= N1 ; :: thesis: f . n <= g . n
n + 0 <= N1 + 1 by A7, XREAL_1:7;
hence f . n <= g . n by A4, A6; :: thesis: verum

end;

N1 + 1 >= (M + 1) + 0 by A2, XREAL_1:7;
then f . (N1 + 1) <= g . (N1 + 1) by A4;
then (Sum (f,N1,M)) + (f . (N1 + 1)) <= (g . (N1 + 1)) + (Sum (g,N1,M)) by A3, A5, XREAL_1:7;
then Sum (f,(N1 + 1),M) <= (g . (N1 + 1)) + (Sum (g,N1,M)) by Lm15;
hence Sum (f,(N1 + 1),M) <= Sum (g,(N1 + 1),M) by Lm15; :: thesis: verum

end;

A8: S₁[M + 1]

proof

A9: Sum (g,(M + 1),M) = (Sum (g,(M + 1))) - (Sum (g,M)) by SERIES_1:def 6
.= ((Partial_Sums g) . (M + 1)) - (Sum (g,M)) by SERIES_1:def 5
.= ((g . (M + 1)) + ((Partial_Sums g) . M)) - (Sum (g,M)) by SERIES_1:def 1
.= ((g . (M + 1)) + (Sum (g,M))) - (Sum (g,M)) by SERIES_1:def 5
.= (g . (M + 1)) + 0 ;
A10: Sum (f,(M + 1),M) = (Sum (f,(M + 1))) - (Sum (f,M)) by SERIES_1:def 6
.= ((Partial_Sums f) . (M + 1)) - (Sum (f,M)) by SERIES_1:def 5
.= ((f . (M + 1)) + ((Partial_Sums f) . M)) - (Sum (f,M)) by SERIES_1:def 1
.= ((f . (M + 1)) + (Sum (f,M))) - (Sum (f,M)) by SERIES_1:def 5
.= (f . (M + 1)) + 0 ;
assume for n being Element of NAT st M + 1 <= n & n <= M + 1 holds
f . n <= g . n ; :: thesis: Sum (f,(M + 1),M) <= Sum (g,(M + 1),M)
hence Sum (f,(M + 1),M) <= Sum (g,(M + 1),M) by A10, A9; :: thesis: verum

end;

for N being Nat st N >= M + 1 holds
S₁[N] from NAT_1:sch 8(A8, A1);
hence for N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds
f . n <= g . n ) holds
Sum (f,N,M) <= Sum (g,N,M) ; :: thesis: verum