let X be non empty set ; 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 Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is E -measurable
let S be 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 Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is E -measurable
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is E -measurable
let E be Element of S; ( dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is E -measurable )
assume that
A1:
dom (f . 0) = E
and
A2:
for n being Nat holds f . n is E -measurable
and
A3:
for x being Element of X st x in E holds
f # x is convergent
; lim f is E -measurable
A4:
lim (Im f) = R_EAL (Im (lim f))
by A1, A3, Th25;
dom ((Im f) . 0) = E
by A1, Def12;
then
lim (Im f) is E -measurable
by A7, A5, Th21;
then A8:
Im (lim f) is E -measurable
by A4, MESFUNC6:def 1;
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 E -measurable
by A11, A9, Th21;
then
Re (lim f) is E -measurable
by A12, MESFUNC6:def 1;
hence
lim f is E -measurable
by A8, MESFUN6C:def 1; verum