let F be Function of NAT , ExtREAL ; :: thesis: ( F is nonnegative implies 0. <= SUM F )
assume A1: F is nonnegative ; :: thesis: 0. <= SUM F
( (Ser F) . 0 in rng (Ser F) & 0. <= (Ser F) . 0 ) by A1, FUNCT_2:6, SUPINF_2:59;
then consider y being R_eal such that
A3: ( y in rng (Ser F) & 0. <= y ) ;
( 0. <= y & y <= sup (rng (Ser F)) ) by A3, XXREAL_2:4;
hence 0. <= SUM F by XXREAL_0:2; :: thesis: verum