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 g being PartFunc 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 ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for g being PartFunc 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 ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,COMPLEX ; :: thesis: for g being PartFunc 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 ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let g be PartFunc 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 ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g 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 ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) implies g 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: dom g = E and
A4: for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ; :: thesis: g is_measurable_on E
B1: dom ((Re f) . 0 ) = E by A1, Def13;

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

end;

B3: dom (Re g) = E by A3, MESFUN6C:def 1;

now

let x be Element of X; :: thesis: ( x in E implies ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) ) )
assume P01: x in E ; :: thesis: ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )
then P02: f # x is convergent by A4;
then Re (f # x) is convergent ;
hence (Re f) # x is convergent by P01, A1, Th7a; :: thesis: (Re g) . x = lim ((Re f) # x)
g . x = lim (f # x) by P01, A4;
then Re (g . x) = lim (Re (f # x)) by P02, COMSEQ_3:41;
then Re (g . x) = lim ((Re f) # x) by P01, A1, Th7a;
hence (Re g) . x = lim ((Re f) # x) by P01, B3, MESFUN6C:def 1; :: thesis: verum

end;

then R_EAL (Re g) is_measurable_on E by B1, B2, B3, Th26;
then B4: Re g is_measurable_on E by MESFUNC6:def 6;
C1: dom ((Im f) . 0 ) = E by A1, Def14;

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

end;

C3: dom (Im g) = E by A3, MESFUN6C:def 2;

now

let x be Element of X; :: thesis: ( x in E implies ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) ) )
assume P01: x in E ; :: thesis: ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )
then P02: f # x is convergent by A4;
then Im (f # x) is convergent ;
hence (Im f) # x is convergent by P01, A1, Th7a; :: thesis: (Im g) . x = lim ((Im f) # x)
g . x = lim (f # x) by P01, A4;
then Im (g . x) = lim (Im (f # x)) by P02, COMSEQ_3:41;
then Im (g . x) = lim ((Im f) # x) by P01, A1, Th7a;
hence (Im g) . x = lim ((Im f) # x) by P01, C3, MESFUN6C:def 2; :: thesis: verum

end;

then R_EAL (Im g) is_measurable_on E by C1, C2, C3, Th26;
then Im g is_measurable_on E by MESFUNC6:def 6;
hence g is_measurable_on E by B4, MESFUN6C:def 3; :: thesis: verum