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 Nat holds f . n is E -measurable ) & 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 E -measurable

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 Nat holds f . n is E -measurable ) & 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 E -measurable

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 Nat holds f . n is E -measurable ) & 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 E -measurable

let g be PartFunc 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 ) & 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 E -measurable

let E be Element of S; :: thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & 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 E -measurable )

assume that

A1: dom (f . 0) = E and

A2: for n being Nat holds f . n is E -measurable 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 E -measurable

then R_EAL (Im g) is E -measurable by A5, A6, A7, Th22;

then A10: Im g is E -measurable by MESFUNC6:def 1;

then R_EAL (Re g) is E -measurable by A11, A12, A13, Th22;

then Re g is E -measurable by MESFUNC6:def 1;

hence g is E -measurable by A10, MESFUN6C:def 1; :: thesis: verum

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 Nat holds f . n is E -measurable ) & 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 E -measurable

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 Nat holds f . n is E -measurable ) & 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 E -measurable

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 Nat holds f . n is E -measurable ) & 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 E -measurable

let g be PartFunc 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 ) & 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 E -measurable

let E be Element of S; :: thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) & 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 E -measurable )

assume that

A1: dom (f . 0) = E and

A2: for n being Nat holds f . n is E -measurable 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 E -measurable

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

A6:
dom (Im g) = E
by A3, COMSEQ_3:def 4;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

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

( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )

dom ((Im f) . 0) = E
by A1, Def12;( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )

let x be Element of X; :: thesis: ( x in E implies ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) ) )

assume A8: x in E ; :: thesis: ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )

then A9: f # x is convergent by A4;

then Im (f # x) is convergent ;

hence (Im f) # x is convergent by A1, A8, Th23; :: thesis: (Im g) . x = lim ((Im f) # x)

g . x = lim (f # x) by A4, A8;

then Im (g . x) = lim (Im (f # x)) by A9, COMSEQ_3:41;

then Im (g . x) = lim ((Im f) # x) by A1, A8, Th23;

hence (Im g) . x = lim ((Im f) # x) by A6, A8, COMSEQ_3:def 4; :: thesis: verum

end;assume A8: x in E ; :: thesis: ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )

then A9: f # x is convergent by A4;

then Im (f # x) is convergent ;

hence (Im f) # x is convergent by A1, A8, Th23; :: thesis: (Im g) . x = lim ((Im f) # x)

g . x = lim (f # x) by A4, A8;

then Im (g . x) = lim (Im (f # x)) by A9, COMSEQ_3:41;

then Im (g . x) = lim ((Im f) # x) by A1, A8, Th23;

hence (Im g) . x = lim ((Im f) # x) by A6, A8, COMSEQ_3:def 4; :: thesis: verum

then R_EAL (Im g) is E -measurable by A5, A6, A7, Th22;

then A10: Im g is E -measurable by MESFUNC6:def 1;

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

A12:
dom (Re g) = E
by A3, COMSEQ_3:def 3;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

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

( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )

dom ((Re f) . 0) = E
by A1, Def11;( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )

let x be Element of X; :: thesis: ( x in E implies ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) ) )

assume A14: x in E ; :: thesis: ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )

then A15: f # x is convergent by A4;

then Re (f # x) is convergent ;

hence (Re f) # x is convergent by A1, A14, Th23; :: thesis: (Re g) . x = lim ((Re f) # x)

g . x = lim (f # x) by A4, A14;

then Re (g . x) = lim (Re (f # x)) by A15, COMSEQ_3:41;

then Re (g . x) = lim ((Re f) # x) by A1, A14, Th23;

hence (Re g) . x = lim ((Re f) # x) by A12, A14, COMSEQ_3:def 3; :: thesis: verum

end;assume A14: x in E ; :: thesis: ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )

then A15: f # x is convergent by A4;

then Re (f # x) is convergent ;

hence (Re f) # x is convergent by A1, A14, Th23; :: thesis: (Re g) . x = lim ((Re f) # x)

g . x = lim (f # x) by A4, A14;

then Re (g . x) = lim (Re (f # x)) by A15, COMSEQ_3:41;

then Re (g . x) = lim ((Re f) # x) by A1, A14, Th23;

hence (Re g) . x = lim ((Re f) # x) by A12, A14, COMSEQ_3:def 3; :: thesis: verum

then R_EAL (Re g) is E -measurable by A11, A12, A13, Th22;

then Re g is E -measurable by MESFUNC6:def 1;

hence g is E -measurable by A10, MESFUN6C:def 1; :: thesis: verum