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 F be with_the_same_dom Functional_Sequence of X,COMPLEX ; :: thesis:
assume that
A1: ( M . E < +infty & E = dom (F . 0 ) ) and
A2: for n being Nat holds F . n is_measurable_on E and
A3: F is uniformly_bounded and
A4: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
A5: ( E = dom ((Re F) . 0 ) & E = dom ((Im F) . 0 ) ) by A1, MESFUN7C:def 12, MESFUN7C:def 11;
A6: for n being Nat holds
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A2, Lm1;
consider K being real number such that
A8: for n being Nat
for x being Element of X st x in dom (F . 0 ) holds
|.((F . n) . x).| <= K by A3, DefUBc;
A9: for x being Element of X st x in E holds
(Re F) # x is convergent

proof

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

end;

A10: for x being Element of X st x in E holds
(Im F) # x is convergent

proof

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

end;

for n being Nat
for x being Element of X st x in dom ((Re F) . 0 ) holds
|.(((Re F) . n) . x).| <= K

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in dom ((Re F) . 0 ) ; :: thesis:
then P1: x in E by A1, MESFUN7C:def 11;
then |.((F . n) . x).| <= K by A1, A8;
then P2: |.((F # x) . n).| <= K by MESFUN7C:def 9;
P3: n is Element of NAT by ORDINAL1:def 13;
then Re ((F # x) . n) = (Re (F # x)) . n by COMSEQ_3:def 3;
then Re ((F # x) . n) = ((Re F) # x) . n by P1, A1, MESFUN7C:23;
then |.(((Re F) # x) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
then |.(((Re F) # x) . n).| <= K by P2, XXREAL_0:2;
hence |.(((Re F) . n) . x).| <= K by P3, SEQFUNC:def 11; :: thesis:

end;

then A11: Re F is uniformly_bounded by DefUBr;
for n being Nat
for x being Element of X st x in dom ((Im F) . 0 ) holds
|.(((Im F) . n) . x).| <= K

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in dom ((Im F) . 0 ) ; :: thesis:
then P1: x in E by A1, MESFUN7C:def 12;
then |.((F . n) . x).| <= K by A1, A8;
then P2: |.((F # x) . n).| <= K by MESFUN7C:def 9;
P3: n is Element of NAT by ORDINAL1:def 13;
then Im ((F # x) . n) = (Im (F # x)) . n by COMSEQ_3:def 4;
then Im ((F # x) . n) = ((Im F) # x) . n by P1, A1, MESFUN7C:23;
then |.(((Im F) # x) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
then |.(((Im F) # x) . n).| <= K by P2, XXREAL_0:2;
hence |.(((Im F) . n) . x).| <= K by P3, SEQFUNC:def 11; :: thesis:

end;

then A12: Im F is uniformly_bounded by DefUBr;
thus T1: for n being Nat holds F . n is_integrable_on M :: thesis:

proof

let n be Nat; :: thesis:
( (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 A1, A5, A6, A9, A10, A11, A12, MES1020r;
hence F . n is_integrable_on M by MESFUN6C:def 4; :: thesis:

end;

A13: ( lim (Re F) is_integrable_on M & lim (Im F) is_integrable_on M ) by A1, A5, A6, A9, A10, A11, A12, MES1020r;
then ( R_EAL (Re (lim F)) is_integrable_on M & R_EAL (Im (lim F)) is_integrable_on M ) by A1, A4, MESFUN7C:25;
then ( Re (lim F) is_integrable_on M & Im (lim F) is_integrable_on M ) by MESFUNC6:def 9;
hence T2: lim F is_integrable_on M by MESFUN6C:def 4; :: thesis:
defpred S₁[ Element of NAT , set ] means $2 = Integral M,(F . $1);
A14: for n being Element of NAT ex y being Element of COMPLEX st S₁[n,y]

proof

let n be Element of NAT ; :: thesis:
take y = Integral M,(F . n); :: thesis:
thus ( y is Element of COMPLEX & S₁[n,y] ) by XCMPLX_0:def 2; :: thesis:

end;

consider I being Function of NAT ,COMPLEX such that
A15: for n being Element of NAT holds S₁[n,I . n] from FUNCT_2:sch 3(A14);
reconsider I = I as Complex_Sequence ;
take I ; :: thesis:
consider A being ExtREAL_sequence such that
A16: ( ( for n being Nat holds A . n = Integral M,((Re F) . n) ) & A is convergent & lim A = Integral M,(lim (Re F)) ) by A1, A5, A6, A9, A11, MES1020r;
consider B being ExtREAL_sequence such that
A17: ( ( for n being Nat holds B . n = Integral M,((Im F) . n) ) & B is convergent & lim B = Integral M,(lim (Im F)) ) by A1, A5, A6, A10, A12, MES1020r;
for n1 being set st n1 in NAT holds
( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

proof

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;
F . n is_integrable_on M by T1;
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;
P3: I . n1 = Integral M,(F . n) by A15;
(Re I) . n = Re (I . n) by COMSEQ_3:def 3;
then (Re I) . n1 = RF by P2, P3, COMPLEX1:28;
hence (R_EAL (Re I)) . n1 = A . n1 by A16, P1, P2; :: thesis:
(Im I) . n = Im (I . n) by COMSEQ_3:def 4;
then (Im I) . n1 = IF by P2, P3, COMPLEX1:28;
hence (R_EAL (Im I)) . n1 = B . n1 by A17, P1, P2; :: thesis:

end;

then ( ( for n1 being set st n1 in NAT holds
(R_EAL (Re I)) . n1 = A . n1 ) & ( for n1 being set st n1 in NAT holds
(R_EAL (Im I)) . n1 = B . n1 ) ) ;
then A18: ( Re I = A & Im I = B ) by FUNCT_2:18;
A19: ( -infty < Integral M,(lim (Re F)) & Integral M,(lim (Re F)) < +infty & -infty < Integral M,(lim (Im F)) & Integral M,(lim (Im F)) < +infty ) by A13, MESFUNC5:102;
thus for n being Nat holds I . n = Integral M,(F . n) :: thesis:

proof

let n be Nat; :: thesis:
P1: I . n = (Re (I . n)) + ((Im (I . n)) * <i> ) by COMPLEX1:29;
n is Element of NAT by ORDINAL1:def 13;
then P2: ( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
( (Re F) . n = Re (F . n) & (Im F) . n = Im (F . n) ) by MESFUN7C:24;
then P3: ( (Re I) . n = Integral M,(Re (F . n)) & (Im I) . n = Integral M,(Im (F . n)) ) by A16, A17, A18;
F . n is_integrable_on M by T1;
hence I . n = Integral M,(F . n) by P1, P2, P3, MESFUN6C:def 5; :: thesis:

end;

A20: now

assume R01: A is convergent ; :: thesis:
assume not A is convergent_to_finite_number ; :: thesis:
then ( A is convergent_to_+infty or A is convergent_to_-infty ) by R01, MESFUNC5:def 11;
hence contradiction by A16, A19, MESFUNC5:def 12; :: thesis:

end;

A21: now

assume R01: B is convergent ; :: thesis:
assume not B is convergent_to_finite_number ; :: thesis:
then ( B is convergent_to_+infty or B is convergent_to_-infty ) by R01, MESFUNC5:def 11;
hence contradiction by A17, A19, MESFUNC5:def 12; :: thesis:

end;

then A22: ( Re I is convergent & Im I is convergent ) by A16, A17, A18, A20, RINFSUP2:15;
hence I is convergent by COMSEQ_3:42; :: thesis:
A23: ( lim (Re I) = Integral M,(lim (Re F)) & lim (Im I) = Integral M,(lim (Im F)) ) by A16, A17, A18, A20, A21, RINFSUP2:15;
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 A24: lim I = (lim (Re I)) + ((lim (Im I)) * <i> ) by A22, 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, A4, MESFUN7C:25;
hence lim I = Integral M,(lim F) by T2, A23, A24, MESFUN6C:def 5; :: thesis: