let X be non empty set ; :: thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for E being Element of S st dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for E being Element of S st dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,COMPLEX ; :: thesis: for E being Element of S st dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let E be Element of S; :: thesis: ( dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is_measurable_on E )
assume that
A1: dom (f . 0 ) = E and
A2: for n being natural number holds f . n is_measurable_on E and
A3: for x being Element of X st x in E holds
f # x is convergent ; :: thesis: lim f is_measurable_on E
A4: lim (Im f) = R_EAL (Im (lim f)) by A1, A3, Th25;

A5: now

let x be Element of X; :: thesis: ( x in E implies (Im f) # x is convergent )
assume A6: x in E ; :: thesis: (Im f) # x is convergent
then f # x is convergent by A3;
then Im (f # x) is convergent ;
hence (Im f) # x is convergent by A1, A6, Th23; :: thesis: verum

end;

A7: now

let n be natural number ; :: thesis: (Im f) . n is_measurable_on E
f . n is_measurable_on E by A2;
then Im (f . n) is_measurable_on E by MESFUN6C:def 3;
hence (Im f) . n is_measurable_on E by Th24; :: thesis: verum

end;

dom ((Im f) . 0 ) = E by A1, Def12;
then lim (Im f) is_measurable_on E by A7, A5, Th21;
then A8: Im (lim f) is_measurable_on E by A4, MESFUNC6:def 6;

A9: now

let x be Element of X; :: thesis: ( x in E implies (Re f) # x is convergent )
assume A10: x in E ; :: thesis: (Re f) # x is convergent
then f # x is convergent by A3;
then Re (f # x) is convergent ;
hence (Re f) # x is convergent by A1, A10, Th23; :: thesis: verum

end;

A11: now

let n be natural number ; :: thesis: (Re f) . n is_measurable_on E
f . n is_measurable_on E by A2;
then Re (f . n) is_measurable_on E by MESFUN6C:def 3;
hence (Re f) . n is_measurable_on E by Th24; :: thesis: verum

end;

A12: lim (Re f) = R_EAL (Re (lim f)) by A1, A3, Th25;
dom ((Re f) . 0 ) = E by A1, Def11;
then lim (Re f) is_measurable_on E by A11, A9, Th21;
then Re (lim f) is_measurable_on E by A12, MESFUNC6:def 6;
hence lim f is_measurable_on E by A8, MESFUN6C:def 3; :: thesis: verum