for F being sequence of ExtREAL st F is nonnegative & SUM F < +infty holds
for n being Element of NAT holds F . n in REAL