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

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:9;
hence f . n <= g . n by A4, A6; :: thesis: verum

end;

N1 + 1 >= (M + 1) + 0 by A2, XREAL_1:9;
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:9;
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 7
.= ((Partial_Sums g) . (M + 1)) - (Sum g,M) by SERIES_1:def 6
.= ((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 6
.= (g . (M + 1)) + 0 ;
A10: Sum f,(M + 1),M = (Sum f,(M + 1)) - (Sum f,M) by SERIES_1:def 7
.= ((Partial_Sums f) . (M + 1)) - (Sum f,M) by SERIES_1:def 6
.= ((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 6
.= (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