theorem :: MESFUN11:68

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,ExtREAL
for E being Element of S
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is E -measurable & F . n is nonpositive & I . n = Integral (M,(F . n)) ) ) holds
Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m