theorem Th37: :: MESFUNC9:37

for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds
((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x