for X being non empty set
for S being SigmaField of X
for P being Element of S
for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds
F /. n is P -measurable ) holds
for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable