let F be Function of NAT,ExtREAL; :: thesis: ( F is nonnegative implies for n being Element of NAT holds (Ser F) . n <= SUM F )
for n being Element of NAT holds F . n <= F . n ;
hence ( F is nonnegative implies for n being Element of NAT holds (Ser F) . n <= SUM F ) by Th6; :: thesis: verum