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
A4: F is additive and
A5: F is with_the_same_dom and
A2: for n being Nat holds (Partial_Sums F) . n is_measurable_on E and
A3: for x being Element of X st x in E holds
F # x is summable ; :: thesis:
P1: dom ((Partial_Sums F) . 0 ) = E by ADD0, A1, A4, A5;
reconsider PF = Partial_Sums F as with_the_same_dom Functional_Sequence of X,ExtREAL by A4, A5, ADD5;

now

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

end;

hence lim (Partial_Sums F) is_measurable_on E by P1, A2, MESFUNC8:25; :: thesis: