theorem Th38: :: MESFUNC9:38

for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) holds
( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )