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

proof

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

A4: now :: thesis: for n being Element of NAT st n <= N holds
f . n <= g . n

let n be Element of NAT ; :: thesis: ( n <= N implies f . n <= g . n )
assume n <= N ; :: thesis: f . n <= g . n
then n + 0 <= N + 1 by XREAL_1:7;
hence f . n <= g . n by A3; :: thesis: verum

end;

f . (N + 1) <= g . (N + 1) by A3;
then (Sum (f,N)) + (f . (N + 1)) <= (Sum (g,N)) + (g . (N + 1)) by A2, A4, XREAL_1:7;
then ((Partial_Sums f) . N) + (f . (N + 1)) <= (Sum (g,N)) + (g . (N + 1)) by SERIES_1:def 5;
then (Partial_Sums f) . (N + 1) <= (Sum (g,N)) + (g . (N + 1)) by SERIES_1:def 1;
then Sum (f,(N + 1)) <= (Sum (g,N)) + (g . (N + 1)) by SERIES_1:def 5;
then Sum (f,(N + 1)) <= ((Partial_Sums g) . N) + (g . (N + 1)) by SERIES_1:def 5;
then Sum (f,(N + 1)) <= (Partial_Sums g) . (N + 1) by SERIES_1:def 1;
hence Sum (f,(N + 1)) <= Sum (g,(N + 1)) by SERIES_1:def 5; :: thesis: verum

end;

A5: S₁[ 0 ]

proof

assume for n being Element of NAT st n <= 0 holds
f . n <= g . n ; :: thesis: Sum (f,0) <= Sum (g,0)
then f . 0 <= g . 0 ;
then (Partial_Sums f) . 0 <= g . 0 by SERIES_1:def 1;
then (Partial_Sums f) . 0 <= (Partial_Sums g) . 0 by SERIES_1:def 1;
then Sum (f,0) <= (Partial_Sums g) . 0 by SERIES_1:def 5;
hence Sum (f,0) <= Sum (g,0) by SERIES_1:def 5; :: thesis: verum

end;

for N being Nat holds S₁[N] from NAT_1:sch 2(A5, A1);
hence for N being Element of NAT st ( for n being Element of NAT st n <= N holds
f . n <= g . n ) holds
Sum (f,N) <= Sum (g,N) ; :: thesis: verum