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₁[ Element of 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 Element of NAT st S₁[N] holds
S₁[N + 1]

proof

let N be Element of 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

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:9;
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:9;
then ((Partial_Sums f) . N) + (f . (N + 1)) <= (Sum g,N) + (g . (N + 1)) by SERIES_1:def 6;
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 6;
then Sum f,(N + 1) <= ((Partial_Sums g) . N) + (g . (N + 1)) by SERIES_1:def 6;
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 6; :: 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 6;
hence Sum f,0 <= Sum g,0 by SERIES_1:def 6; :: thesis: verum

end;

for N being Element of NAT holds S₁[N] from NAT_1:sch 1(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