theorem Th2: :: MEASURE7:2

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