let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let M be sigma_Measure of S; :: thesis: for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let E be Element of S; :: thesis: for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let P be PartFunc of X,REAL; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) implies lim F is_integrable_on M )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is E -measurable and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A6: for x being Element of X st x in E holds
F # x is convergent ; :: thesis: lim F is_integrable_on M
A7: for n being Nat holds
( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;
for x being Element of X
for n being Nat st x in E holds
( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

proof

let x be Element of X; :: thesis: for n being Nat st x in E holds
( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
let n be Nat; :: thesis: ( x in E implies ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
Re ((F # x) . n1) = (Re (F # x)) . n1 by COMSEQ_3:def 5;
then A8: |.((Re (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
Im ((F # x) . n1) = (Im (F # x)) . n1 by COMSEQ_3:def 6;
then A9: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
assume A10: x in E ; :: thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
then |.(F . n).| . x <= P . x by A5;
then |.((F . n) . x).| <= P . x by VALUED_1:18;
then A11: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;
(Im F) # x = Im (F # x) by A1, A10, MESFUN7C:23;
then |.(((Im F) # x) . n1).| <= P . x by A11, A9, XXREAL_0:2;
then A12: |.(((Im F) . n1) . x).| <= P . x by SEQFUNC:def 10;
(Re F) # x = Re (F # x) by A1, A10, MESFUN7C:23;
then |.(((Re F) # x) . n1).| <= P . x by A11, A8, XXREAL_0:2;
then |.(((Re F) . n1) . x).| <= P . x by SEQFUNC:def 10;
hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A12, VALUED_1:18; :: thesis: verum

end;

then A13: for x being Element of X
for n being Nat holds
( ( x in E implies |.((Re F) . n).| . x <= P . x ) & ( x in E implies |.((Im F) . n).| . x <= P . x ) ) ;
A14: for x being Element of X st x in E holds
( (Re F) # x is convergent & (Im F) # x is convergent )

proof

let x be Element of X; :: thesis: ( x in E implies ( (Re F) # x is convergent & (Im F) # x is convergent ) )
assume A15: x in E ; :: thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )
then F # x is convergent Complex_Sequence by A6;
then ( Re (F # x) is convergent & Im (F # x) is convergent ) ;
hence ( (Re F) # x is convergent & (Im F) # x is convergent ) by A1, A15, MESFUN7C:23; :: thesis: verum

end;

then A16: for x being Element of X st x in E holds
(Im F) # x is convergent ;
E = dom ((Im F) . 0) by A1, MESFUN7C:def 12;
then lim (Im F) is_integrable_on M by A2, A4, A7, A13, A16, Th47;
then R_EAL (Im (lim F)) is_integrable_on M by A1, A6, MESFUN7C:25;
then A17: Im (lim F) is_integrable_on M ;
A18: for x being Element of X st x in E holds
(Re F) # x is convergent by A14;
E = dom ((Re F) . 0) by A1, MESFUN7C:def 11;
then lim (Re F) is_integrable_on M by A2, A4, A7, A13, A18, Th47;
then R_EAL (Re (lim F)) is_integrable_on M by A1, A6, MESFUN7C:25;
then Re (lim F) is_integrable_on M ;
hence lim F is_integrable_on M by A17, MESFUN6C:def 2; :: thesis: verum