let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let P be PartFunc of X,REAL; :: thesis:
let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis:
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 ; :: thesis:
A6: E = dom ((Re F) . 0) by A1, MESFUN7C:def 11;
A7: for n being Nat holds
( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;
A8: 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 )

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
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 A9: |.((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 A10: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
assume A11: x in E ; :: thesis:
then |.(F . n).| . x <= P . x by A5;
then |.((F . n) . x).| <= P . x by VALUED_1:18;
then A12: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;
(Im F) # x = Im (F # x) by A1, A11, MESFUN7C:23;
then A13: |.(((Im F) # x) . n1).| <= P . x by A12, A10, XXREAL_0:2;
(Re F) # x = Re (F # x) by A1, A11, MESFUN7C:23;
then |.(((Re F) # x) . n).| <= P . x by A12, A9, XXREAL_0:2;
then A14: |.(((Re F) . n) . x).| <= P . x by SEQFUNC:def 10;
|.(((Im F) . n) . x).| <= P . x by A13, SEQFUNC:def 10;
hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A14, VALUED_1:18; :: thesis:

end;

then for x being Element of X
for n being Nat st x in E holds
|.((Re F) . n).| . x <= P . x ;
then consider A being Real_Sequence such that
A15: for n being Nat holds A . n = Integral (M,((Re F) . n)) and
A16: ( ( for x being Element of X st x in E holds
(Re F) # x is convergent ) implies ( A is convergent & lim A = Integral (M,(lim (Re F))) ) ) by A2, A4, A6, A7, Th48;
defpred S₁[ Element of NAT , set ] means $2 = Integral (M,(F . $1));
A17: for n being Element of NAT ex y being Element of COMPLEX st S₁[n,y]

let n be Element of NAT ; :: thesis:
Integral (M,(F . n)) is Element of COMPLEX by XCMPLX_0:def 2;
hence ex y being Element of COMPLEX st S₁[n,y] ; :: thesis:

end;

consider I being sequence of COMPLEX such that
A18: for n being Element of NAT holds S₁[n,I . n] from FUNCT_2:sch 3(A17);
reconsider I = I as Complex_Sequence ;
A19: E = dom ((Im F) . 0) by A1, MESFUN7C:def 12;
for x being Element of X
for n being Nat st x in E holds
|.((Im F) . n).| . x <= P . x by A8;
then consider B being Real_Sequence such that
A20: for n being Nat holds B . n = Integral (M,((Im F) . n)) and
A21: ( ( for x being Element of X st x in E holds
(Im F) # x is convergent ) implies ( B is convergent & lim B = Integral (M,(lim (Im F))) ) ) by A2, A4, A19, A7, Th48;
A22: for n being Nat holds
( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M )

let n be Nat; :: thesis:

A23: now :: thesis:

let x be Element of X; :: thesis:
assume x in dom ((Re F) . n) ; :: thesis:
then x in E by A6, MESFUNC8:def 2;
then |.((Re F) . n).| . x <= P . x by A8;
hence |.(((Re F) . n) . x).| <= P . x by VALUED_1:18; :: thesis:

end;

A24: now :: thesis:

let x be Element of X; :: thesis:
assume x in dom ((Im F) . n) ; :: thesis:
then x in E by A19, MESFUNC8:def 2;
then |.((Im F) . n).| . x <= P . x by A8;
hence |.(((Im F) . n) . x).| <= P . x by VALUED_1:18; :: thesis:

end;

A25: ( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;
( dom ((Re F) . n) = E & dom ((Im F) . n) = E ) by A6, A19, MESFUNC8:def 2;
hence ( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M ) by A2, A4, A23, A24, A25, MESFUNC6:96; :: thesis:

end;

A26: now :: thesis:

let n1 be set ; :: thesis:
assume n1 in NAT ; :: thesis:
then reconsider n = n1 as Element of NAT ;
A27: ( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;
A28: (Im F) . n = Im (F . n) by MESFUN7C:24;
then A29: Im (F . n) is_integrable_on M by A22;
A30: (Re F) . n = Re (F . n) by MESFUN7C:24;
then Re (F . n) is_integrable_on M by A22;
then F . n is_integrable_on M by A29, MESFUN6C:def 2;
then consider RF, IF being Real such that
A31: ( RF = Integral (M,(Re (F . n))) & IF = Integral (M,(Im (F . n))) ) and
A32: Integral (M,(F . n)) = RF + (IF * <i>) by MESFUN6C:def 3;
I . n1 = Integral (M,(F . n)) by A18;
then ( Re (I . n1) = RF & Im (I . n1) = IF ) by A32, COMPLEX1:12;
hence ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 ) by A15, A20, A30, A28, A31, A27; :: thesis:

end;

then for x being object st x in NAT holds
(Re I) . x = A . x ;
then A33: Re I = A ;
take I ; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence I . n = Integral (M,(F . n)) by A18; :: thesis:

end;

for x being object st x in NAT holds
(Im I) . x = B . x by A26;
then A34: Im I = B ;

hereby :: thesis:

assume A35: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
then A36: Integral (M,(lim (Im F))) = Integral (M,(Im (lim F))) by A1, MESFUN7C:25;
A37: ( lim F is_integrable_on M & Integral (M,(lim (Re F))) = Integral (M,(Re (lim F))) ) by A1, A2, A3, A4, A5, A35, Th51, MESFUN7C:25;

A38: now :: thesis:

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

end;

hence I is convergent by A16, A21, A33, A34, COMSEQ_3:42; :: thesis:
for n being Nat holds
( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;
then lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A16, A21, A33, A34, A38, COMSEQ_3:39;
hence lim I = Integral (M,(lim F)) by A16, A21, A33, A34, A38, A37, A36, MESFUN6C:def 3; :: thesis:

end;