let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is E -measurable
let S be SigmaField of X; :: thesis: for E being Element of S
for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is E -measurable
let E be Element of S; :: thesis: for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is E -measurable
let F be Functional_Sequence of X,REAL; :: thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds
F # x is summable ) implies lim (Partial_Sums F) is E -measurable )
assume that
A1: ( dom (F . 0) = E & F is with_the_same_dom ) and
A2: for n being Nat holds (Partial_Sums F) . n is E -measurable and
A3: for x being Element of X st x in E holds
F # x is summable ; :: thesis: lim (Partial_Sums F) is E -measurable

A4: now :: thesis: for x being Element of X st x in E holds
(Partial_Sums F) # x is convergent

let x be Element of X; :: thesis: ( x in E implies (Partial_Sums F) # x is convergent )
assume A5: x in E ; :: thesis: (Partial_Sums F) # x is convergent
then F # x is summable by A3;
then Partial_Sums (F # x) is convergent ;
hence (Partial_Sums F) # x is convergent by A1, A5, Th13; :: thesis: verum

end;

( dom ((Partial_Sums F) . 0) = E & Partial_Sums F is with_the_same_dom Functional_Sequence of X,REAL ) by A1, Th11, Th17;
hence lim (Partial_Sums F) is E -measurable by A2, A4, MESFUN7C:21; :: thesis: verum