theorem Th16: :: MESFUN9C:16

for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL
for m being Nat st ( for n being Nat holds F . n is E -measurable ) holds
(Partial_Sums F) . m is E -measurable