theorem Th67: :: MESFUN11:67

for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for E being Element of S
for m being Nat st F is with_the_same_dom & E = dom (F . 0) & ( for n being Nat holds
( F . n is E -measurable & F . n is without+infty ) ) holds
(Partial_Sums F) . m is E -measurable