let f be Real_Sequence; :: thesis: for N being Element of NAT st ( for n being Element of NAT st n <= N holds
f . n >= 0 ) holds
Sum (f,N) >= 0
defpred S₁[ Nat] means ( ( for n being Element of NAT st n <= $1 holds
f . n >= 0 ) implies Sum (f,$1) >= 0 );
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 >= 0 ) implies Sum (f,N) >= 0 ) ; :: thesis: S₁[N + 1]
assume A3: for n being Element of NAT st n <= N + 1 holds
f . n >= 0 ; :: thesis: Sum (f,(N + 1)) >= 0

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

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

end;

f . (N + 1) >= 0 by A3;
then (Sum (f,N)) + (f . (N + 1)) >= 0 + 0 by A2, A4;
then ((Partial_Sums f) . N) + (f . (N + 1)) >= 0 by SERIES_1:def 5;
then (Partial_Sums f) . (N + 1) >= 0 by SERIES_1:def 1;
hence Sum (f,(N + 1)) >= 0 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 >= 0 ; :: thesis: Sum (f,0) >= 0
then f . 0 >= 0 ;
then (Partial_Sums f) . 0 >= 0 by SERIES_1:def 1;
hence Sum (f,0) >= 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 >= 0 ) holds
Sum (f,N) >= 0 ; :: thesis: verum