let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies 0. <= SUM F )
assume F is nonnegative ; :: thesis: 0. <= SUM F
then 0. <= (Ser F) . 0 by SUPINF_2:40;
hence 0. <= SUM F by FUNCT_2:4, XXREAL_2:4; :: thesis: verum