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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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 ) & E = dom P ) and
A2: for n being Nat holds F . n is_measurable_on E and
A3: P is_integrable_on M and
A4: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A5: for x being Element of X st x in E holds
F # x is convergent ; :: thesis: lim F is_integrable_on M
B1: ( E = dom ((Re F) . 0 ) & E = dom ((Im F) . 0 ) ) by A1, MESFUN7C:def 12, MESFUN7C:def 11;
B2: for n being Nat holds
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A2, Lm1;
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 ) )
assume P1: x in E ; :: thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
then |.(F . n).| . x <= P . x by A4;
then |.((F . n) . x).| <= P . x by VALUED_1:18;
then P2: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
( Re ((F # x) . n1) = (Re (F # x)) . n1 & Im ((F # x) . n1) = (Im (F # x)) . n1 ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
then P3: ( |.((Re (F # x)) . n).| <= |.((F # x) . n).| & |.((Im (F # x)) . n).| <= |.((F # x) . n).| ) by COMSEQ_3:13;
( (Re F) # x = Re (F # x) & (Im F) # x = Im (F # x) ) by A1, P1, MESFUN7C:23;
then ( |.(((Re F) # x) . n1).| <= P . x & |.(((Im F) # x) . n1).| <= P . x ) by P2, P3, XXREAL_0:2;
then ( |.(((Re F) . n1) . x).| <= P . x & |.(((Im F) . n1) . x).| <= P . x ) by SEQFUNC:def 11;
hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by VALUED_1:18; :: thesis: verum

end;

then B3: 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 ) ) ;
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 P01: x in E ; :: thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )
then F # x is convergent Complex_Sequence by A5;
then ( Re (F # x) is convergent & Im (F # x) is convergent ) ;
hence ( (Re F) # x is convergent & (Im F) # x is convergent ) by P01, A1, MESFUN7C:23; :: thesis: verum

end;

then ( ( for x being Element of X st x in E holds
(Re F) # x is convergent ) & ( for x being Element of X st x in E holds
(Im F) # x is convergent ) ) ;
then ( lim (Re F) is_integrable_on M & lim (Im F) is_integrable_on M ) by A1, A3, B1, B2, B3, MES1017r;
then ( R_EAL (Re (lim F)) is_integrable_on M & R_EAL (Im (lim F)) is_integrable_on M ) by A1, A5, MESFUN7C:25;
then ( Re (lim F) is_integrable_on M & Im (lim F) is_integrable_on M ) by MESFUNC6:def 9;
hence lim F is_integrable_on M by MESFUN6C:def 4; :: thesis: verum