for F being sequence of ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds
SUM F = +infty