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: S₁[M + 1]

proof

assume A2: 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
A3: 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 ;
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 ;
hence Sum f,(M + 1),M <= Sum g,(M + 1),M by A2, A3; :: thesis: verum

end;

A4: 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
A5: N1 >= M + 1 and
A6: ( ( 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 A7: 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

A8: now

let n be Element of NAT ; :: thesis: ( M + 1 <= n & n <= N1 implies f . n <= g . n )
assume A9: ( M + 1 <= n & n <= N1 ) ; :: thesis: f . n <= g . n
then n + 0 <= N1 + 1 by XREAL_1:9;
hence f . n <= g . n by A7, A9; :: thesis: verum

end;

N1 + 1 >= (M + 1) + 0 by A5, XREAL_1:9;
then f . (N1 + 1) <= g . (N1 + 1) by A7;
then (Sum f,N1,M) + (f . (N1 + 1)) <= (g . (N1 + 1)) + (Sum g,N1,M) by A6, A8, XREAL_1:9;
then Sum f,(N1 + 1),M <= (g . (N1 + 1)) + (Sum g,N1,M) by Lm20;
hence Sum f,(N1 + 1),M <= Sum g,(N1 + 1),M by Lm20; :: thesis: verum

end;

for N being Nat st N >= M + 1 holds
S₁[N] from NAT_1:sch 8(A1, A4);
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