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 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; :: 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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: lim f is E -measurable

A4: lim (Im f) = R_EAL (Im (lim f)) by A1, A3, Th25;

then lim (Im f) is E -measurable by A7, A5, Th21;

then A8: Im (lim f) is E -measurable by A4, MESFUNC6:def 1;

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; :: thesis: verum

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; :: 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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: lim f is E -measurable

A4: lim (Im f) = R_EAL (Im (lim f)) by A1, A3, Th25;

A5: now :: thesis: for x being Element of X st x in E holds

(Im f) # x is convergent

(Im f) # x is convergent

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;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

A7: now :: thesis: for n being Nat holds (Im f) . n is E -measurable

dom ((Im f) . 0) = E
by A1, Def12;let n be Nat; :: thesis: (Im f) . n is E -measurable

f . n is E -measurable by A2;

then Im (f . n) is E -measurable by MESFUN6C:def 1;

hence (Im f) . n is E -measurable by Th24; :: thesis: verum

end;f . n is E -measurable by A2;

then Im (f . n) is E -measurable by MESFUN6C:def 1;

hence (Im f) . n is E -measurable by Th24; :: thesis: verum

then lim (Im f) is E -measurable by A7, A5, Th21;

then A8: Im (lim f) is E -measurable by A4, MESFUNC6:def 1;

A9: now :: thesis: for x being Element of X st x in E holds

(Re f) # x is convergent

(Re f) # x is convergent

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;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

A11: now :: thesis: for n being Nat holds (Re f) . n is E -measurable

A12:
lim (Re f) = R_EAL (Re (lim f))
by A1, A3, Th25;let n be Nat; :: thesis: (Re f) . n is E -measurable

f . n is E -measurable by A2;

then Re (f . n) is E -measurable by MESFUN6C:def 1;

hence (Re f) . n is E -measurable by Th24; :: thesis: verum

end;f . n is E -measurable by A2;

then Re (f . n) is E -measurable by MESFUN6C:def 1;

hence (Re f) . n is E -measurable by Th24; :: thesis: verum

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; :: thesis: verum