theorem Th6: :: MEASURE7:6

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