theorem :: ASYMPT_1:70

for f being Real_Sequence
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 by Lm12;