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 ) & 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 ; :: thesis:
defpred S₁[ Element of NAT , set ] means $2 = Integral M,(F . $1);
K0: 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 Function of NAT ,COMPLEX such that
K1: for n being Element of NAT holds S₁[n,I . n] from FUNCT_2:sch 3(K0);
reconsider I = I as Complex_Sequence ;
take I ; :: thesis:

hereby :: thesis:

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

end;

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;
B3: 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:
assume P1: x in E ; :: thesis:
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) . n).| <= P . x & |.(((Im F) # x) . n1).| <= P . x ) by P2, P3, XXREAL_0:2;
then ( |.(((Re F) . n) . x).| <= P . x & |.(((Im F) . n) . 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:

end;

let n be Nat; :: thesis:

P1: now

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

end;

P3: now

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

end;

P2: ( dom ((Re F) . n) = E & dom ((Im F) . n) = E ) by B1, MESFUNC8:def 2;
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A2, Lm1;
hence ( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M ) by A1, A3, P1, P2, P3, MESFUNC6:96; :: thesis:

end;

for x being Element of X
for n being Nat st x in E holds
|.((Re F) . n).| . x <= P . x by B3;
then consider A being Real_Sequence such that
B5: ( ( for n being Nat holds A . n = Integral M,((Re F) . n) ) & ( ( 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 A1, A3, B1, B2, MES1018r;
for x being Element of X
for n being Nat st x in E holds
|.((Im F) . n).| . x <= P . x by B3;
then consider B being Real_Sequence such that
B6: ( ( for n being Nat holds B . n = Integral M,((Im F) . n) ) & ( ( 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 A1, A3, B1, B2, MES1018r;

let n1 be set ; :: thesis:
assume n1 in NAT ; :: thesis:
then reconsider n = n1 as Element of NAT ;
P1: ( (Re F) . n = Re (F . n) & (Im F) . n = Im (F . n) ) by MESFUN7C:24;
then ( Re (F . n) is_integrable_on M & Im (F . n) is_integrable_on M ) by B4;
then F . n is_integrable_on M by MESFUN6C:def 4;
then consider RF, IF being Real such that
P2: ( RF = Integral M,(Re (F . n)) & IF = Integral M,(Im (F . n)) & Integral M,(F . n) = RF + (IF * <i> ) ) by MESFUN6C:def 5;
I . n1 = Integral M,(F . n) by K1;
then P3: ( Re (I . n1) = RF & Im (I . n1) = IF ) by P2, COMPLEX1:28;
( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
hence ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 ) by B5, B6, P1, P2, P3; :: thesis:

end;

then ( ( for x being set st x in NAT holds
(Re I) . x = A . x ) & ( for x being set st x in NAT holds
(Im I) . x = B . x ) ) ;
then B7: ( Re I = A & Im I = B ) by FUNCT_2:18;

hereby :: thesis:

assume C1: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:

C2: now

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

end;

hence I is convergent by B7, B5, B6, COMSEQ_3:42; :: thesis:
C3: lim F is_integrable_on M by A1, A2, A3, A4, C1, MES1017c;
for n being Element of NAT holds
( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
then C4: lim I = (lim (Re I)) + ((lim (Im I)) * <i> ) by B7, B5, B6, C2, COMSEQ_3:39;
( Integral M,(lim (Re F)) = Integral M,(Re (lim F)) & Integral M,(lim (Im F)) = Integral M,(Im (lim F)) ) by A1, C1, MESFUN7C:25;
hence lim I = Integral M,(lim F) by B7, B5, B6, C2, C3, C4, MESFUN6C:def 5; :: thesis:

end;