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₁[ Element of NAT ] means ( ( for n being Element of NAT st n <= $1 holds
f . n >= 0 ) implies Sum f,$1 >= 0 );
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 >= 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

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