theorem Th47: :: SUPINF_2:48

for F being sequence of ExtREAL st F is nonnegative holds
for n being Nat st ( for r being Element of NAT st n <= r holds
F . r = 0. ) holds
SUM F = (Ser F) . n