let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let E be Element of S; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
assume that
A1: dom (F . 0) = E and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n being Nat holds (Partial_Sums F) . n is E -measurable and
A5: for x being Element of X st x in E holds
F # x is summable ; :: thesis:
reconsider PF = Partial_Sums F as with_the_same_dom Functional_Sequence of X,ExtREAL by A2, A3, Th43;

A6: now :: thesis:

let x be Element of X; :: thesis:
assume A7: x in E ; :: thesis:
then F # x is summable by A5;
then Partial_Sums (F # x) is convergent ;
hence PF # x is convergent by A1, A2, A3, A7, Th33; :: thesis:

end;

dom ((Partial_Sums F) . 0) = E by A1, A2, A3, Th29;
hence lim (Partial_Sums F) is E -measurable by A4, A6, MESFUNC8:25; :: thesis: