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 and
A2: E = dom (F . 0 ) and
A3: for n being Nat holds F . n is_measurable_on E and
A4: F is uniformly_bounded and
A5: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
consider K being real number such that
A6: for n being Nat
for x being Element of X st x in dom (F . 0 ) holds
|.((F . n) . x).| <= K by A4, Def6;
A7: for x being Element of X st x in E holds
(Re F) # x is convergent

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

end;

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

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in dom ((Im F) . 0 ) ; :: thesis:
then A9: x in E by A2, MESFUN7C:def 12;
then |.((F . n) . x).| <= K by A2, A6;
then A10: |.((F # x) . n).| <= K by MESFUN7C:def 9;
A11: 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 A2, A9, MESFUN7C:23;
then |.(((Im F) # x) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
then |.(((Im F) # x) . n).| <= K by A10, XXREAL_0:2;
hence |.(((Im F) . n) . x).| <= K by A11, SEQFUNC:def 11; :: thesis:

end;

then A12: Im F is uniformly_bounded by Def4;
A13: for x being Element of X st x in E holds
(Im F) # x is convergent

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

end;

defpred S₁[ Element of NAT , set ] means $2 = Integral M,(F . $1);
A15: for n being Element of NAT ex y being Element of COMPLEX st S₁[n,y]

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
A16: for n being Element of NAT holds S₁[n,I . n] from FUNCT_2:sch 3(A15);
reconsider I = I as Complex_Sequence ;
A17: for n being Nat holds
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A3, Lm2;
for n being Nat
for x being Element of X st x in dom ((Re F) . 0 ) holds
|.(((Re F) . n) . x).| <= K

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in dom ((Re F) . 0 ) ; :: thesis:
then A18: x in E by A2, MESFUN7C:def 11;
then |.((F . n) . x).| <= K by A2, A6;
then A19: |.((F # x) . n).| <= K by MESFUN7C:def 9;
A20: 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 A2, A18, MESFUN7C:23;
then |.(((Re F) # x) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
then |.(((Re F) # x) . n).| <= K by A19, XXREAL_0:2;
hence |.(((Re F) . n) . x).| <= K by A20, SEQFUNC:def 11; :: thesis:

end;

then A21: Re F is uniformly_bounded by Def4;
A22: E = dom ((Im F) . 0 ) by A2, MESFUN7C:def 12;
then consider B being ExtREAL_sequence such that
A23: for n being Nat holds B . n = Integral M,((Im F) . n) and
A24: B is convergent and
A25: lim B = Integral M,(lim (Im F)) by A1, A17, A13, A12, Th49;
A26: lim (Im F) is_integrable_on M by A1, A22, A17, A13, A12, Th49;
then R_EAL (Im (lim F)) is_integrable_on M by A2, A5, MESFUN7C:25;
then A27: Im (lim F) is_integrable_on M by MESFUNC6:def 9;
A28: E = dom ((Re F) . 0 ) by A2, MESFUN7C:def 11;
then consider A being ExtREAL_sequence such that
A29: for n being Nat holds A . n = Integral M,((Re F) . n) and
A30: A is convergent and
A31: lim A = Integral M,(lim (Re F)) by A1, A17, A7, A21, Th49;
thus A32: for n being Nat holds F . n is_integrable_on M :: thesis:

let n be Nat; :: thesis:
(Im F) . n = Im (F . n) by MESFUN7C:24;
then A33: Im (F . n) is_integrable_on M by A1, A22, A17, A13, A12, Th49;
(Re F) . n = Re (F . n) by MESFUN7C:24;
then Re (F . n) is_integrable_on M by A1, A28, A17, A7, A21, Th49;
hence F . n is_integrable_on M by A33, MESFUN6C:def 4; :: thesis:

end;

A34: for n1 being set st n1 in NAT holds
( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

let n1 be set ; :: thesis:
assume n1 in NAT ; :: thesis:
then reconsider n = n1 as Element of NAT ;
A35: I . n1 = Integral M,(F . n) by A16;
F . n is_integrable_on M by A32;
then consider RF, IF being Real such that
A36: RF = Integral M,(Re (F . n)) and
A37: IF = Integral M,(Im (F . n)) and
A38: Integral M,(F . n) = RF + (IF * <i> ) by MESFUN6C:def 5;
(Re I) . n = Re (I . n) by COMSEQ_3:def 3;
then ( (Re F) . n = Re (F . n) & (Re I) . n1 = RF ) by A38, A35, COMPLEX1:28, MESFUN7C:24;
hence (R_EAL (Re I)) . n1 = A . n1 by A29, A36; :: thesis:
(Im I) . n = Im (I . n) by COMSEQ_3:def 4;
then ( (Im F) . n = Im (F . n) & (Im I) . n1 = IF ) by A38, A35, COMPLEX1:28, MESFUN7C:24;
hence (R_EAL (Im I)) . n1 = B . n1 by A23, A37; :: thesis:

end;

then for n1 being set st n1 in NAT holds
(R_EAL (Im I)) . n1 = B . n1 ;
then A39: Im I = B by FUNCT_2:18;
A40: ( -infty < Integral M,(lim (Im F)) & Integral M,(lim (Im F)) < +infty ) by A26, MESFUNC5:102;

A41: now

assume A42: 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 A42, MESFUNC5:def 11;
hence contradiction by A24, A25, A40, MESFUNC5:def 12; :: thesis:

end;

then A43: lim (Im I) = Integral M,(lim (Im F)) by A24, A25, A39, RINFSUP2:15;
A44: Im I is convergent by A24, A39, A41, RINFSUP2:15;
A45: lim (Re F) is_integrable_on M by A1, A28, A17, A7, A21, Th49;
then R_EAL (Re (lim F)) is_integrable_on M by A2, A5, MESFUN7C:25;
then Re (lim F) is_integrable_on M by MESFUNC6:def 9;
hence A46: lim F is_integrable_on M by A27, MESFUN6C:def 4; :: thesis:
take I ; :: thesis:
for n1 being set st n1 in NAT holds
(R_EAL (Re I)) . n1 = A . n1 by A34;
then A47: Re I = A by FUNCT_2:18;
thus for n being Nat holds I . n = Integral M,(F . n) :: thesis:

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 13;
then A48: ( (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) by MESFUN7C:24;
then A49: (Re I) . n = Integral M,(Re (F . n)) by A29, A47;
(Im F) . n = Im (F . n) by MESFUN7C:24;
then A50: (Im I) . n = Integral M,(Im (F . n)) by A23, A39;
( I . n = (Re (I . n)) + ((Im (I . n)) * <i> ) & F . n is_integrable_on M ) by A32, COMPLEX1:29;
hence I . n = Integral M,(F . n) by A48, A49, A50, MESFUN6C:def 5; :: thesis:

end;

A51: ( -infty < Integral M,(lim (Re F)) & Integral M,(lim (Re F)) < +infty ) by A45, MESFUNC5:102;

A52: now

assume A53: 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 A53, MESFUNC5:def 11;
hence contradiction by A30, A31, A51, MESFUNC5:def 12; :: thesis:

end;

then A54: Re I is convergent by A30, A47, RINFSUP2:15;
hence I is convergent by A44, COMSEQ_3:42; :: thesis:
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 A55: lim I = (lim (Re I)) + ((lim (Im I)) * <i> ) by A54, A44, COMSEQ_3:39;
A56: ( Integral M,(lim (Re F)) = Integral M,(Re (lim F)) & Integral M,(lim (Im F)) = Integral M,(Im (lim F)) ) by A2, A5, MESFUN7C:25;
lim (Re I) = Integral M,(lim (Re F)) by A30, A31, A47, A52, RINFSUP2:15;
hence lim I = Integral M,(lim F) by A46, A43, A55, A56, MESFUN6C:def 5; :: thesis: