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 E -measurable 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 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;
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;
Im ((F # x) . n) = (Im (F # x)) . n by COMSEQ_3:def 6;
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 SEQFUNC:def 10; :: thesis:

end;

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

let x be Element of X; :: thesis:
assume A13: 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, A13, MESFUN7C:23; :: thesis:

end;

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]

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

end;

consider I being sequence of 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 ;
A16: for n being Nat holds
( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) 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 A17: x in E by A2, MESFUN7C:def 11;
then |.((F . n) . x).| <= K by A2, A6;
then A18: |.((F # x) . n).| <= K by MESFUN7C:def 9;
Re ((F # x) . n) = (Re (F # x)) . n by COMSEQ_3:def 5;
then Re ((F # x) . n) = ((Re F) # x) . n by A2, A17, MESFUN7C:23;
then |.(((Re F) # x) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
then |.(((Re F) # x) . n).| <= K by A18, XXREAL_0:2;
hence |.(((Re F) . n) . x).| <= K by SEQFUNC:def 10; :: thesis:

end;

then A19: Re F is uniformly_bounded ;
A20: E = dom ((Im F) . 0) by A2, MESFUN7C:def 12;
then consider B being ExtREAL_sequence such that
A21: for n being Nat holds B . n = Integral (M,((Im F) . n)) and
A22: B is convergent and
A23: lim B = Integral (M,(lim (Im F))) by A1, A16, A12, A11, Th49;
A24: lim (Im F) is_integrable_on M by A1, A20, A16, A12, A11, Th49;
then R_EAL (Im (lim F)) is_integrable_on M by A2, A5, MESFUN7C:25;
then A25: Im (lim F) is_integrable_on M ;
A26: E = dom ((Re F) . 0) by A2, MESFUN7C:def 11;
then consider A being ExtREAL_sequence such that
A27: for n being Nat holds A . n = Integral (M,((Re F) . n)) and
A28: A is convergent and
A29: lim A = Integral (M,(lim (Re F))) by A1, A16, A7, A19, Th49;
thus A30: 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 A31: Im (F . n) is_integrable_on M by A1, A20, A16, A12, A11, Th49;
(Re F) . n = Re (F . n) by MESFUN7C:24;
then Re (F . n) is_integrable_on M by A1, A26, A16, A7, A19, Th49;
hence F . n is_integrable_on M by A31, MESFUN6C:def 2; :: thesis:

end;

A32: 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 ;
A33: I . n1 = Integral (M,(F . n)) by A15;
F . n is_integrable_on M by A30;
then consider RF, IF being Real such that
A34: RF = Integral (M,(Re (F . n))) and
A35: IF = Integral (M,(Im (F . n))) and
A36: Integral (M,(F . n)) = RF + (IF * <i>) by MESFUN6C:def 3;
(Re I) . n = Re (I . n) by COMSEQ_3:def 5;
then ( (Re F) . n = Re (F . n) & (Re I) . n1 = RF ) by A36, A33, COMPLEX1:12, MESFUN7C:24;
hence (R_EAL (Re I)) . n1 = A . n1 by A27, A34; :: thesis:
(Im I) . n = Im (I . n) by COMSEQ_3:def 6;
then ( (Im F) . n = Im (F . n) & (Im I) . n1 = IF ) by A36, A33, COMPLEX1:12, MESFUN7C:24;
hence (R_EAL (Im I)) . n1 = B . n1 by A21, A35; :: thesis:

end;

then for n1 being object st n1 in NAT holds
(R_EAL (Im I)) . n1 = B . n1 ;
then A37: Im I = B ;
A38: ( -infty < Integral (M,(lim (Im F))) & Integral (M,(lim (Im F))) < +infty ) by A24, MESFUNC5:96;
A39: ( B is convergent implies B is convergent_to_finite_number ) by A23, A38, MESFUNC5:def 12;
then A40: lim (Im I) = Integral (M,(lim (Im F))) by A22, A23, A37, RINFSUP2:15;
A41: Im I is convergent by A22, A37, A39, RINFSUP2:15;
A42: lim (Re F) is_integrable_on M by A1, A26, A16, A7, A19, Th49;
then R_EAL (Re (lim F)) is_integrable_on M by A2, A5, MESFUN7C:25;
then Re (lim F) is_integrable_on M ;
hence A43: lim F is_integrable_on M by A25, MESFUN6C:def 2; :: thesis:
take I ; :: thesis:
for n1 being object st n1 in NAT holds
(R_EAL (Re I)) . n1 = A . n1 by A32;
then A44: Re I = A ;
thus for n being Nat holds I . n = Integral (M,(F . n)) :: thesis:

let n be Nat; :: thesis:
A45: ( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;
(Re F) . n = Re (F . n) by MESFUN7C:24;
then A46: (Re I) . n = Integral (M,(Re (F . n))) by A27, A44;
(Im F) . n = Im (F . n) by MESFUN7C:24;
then A47: (Im I) . n = Integral (M,(Im (F . n))) by A21, A37;
( I . n = (Re (I . n)) + ((Im (I . n)) * <i>) & F . n is_integrable_on M ) by A30, COMPLEX1:13;
hence I . n = Integral (M,(F . n)) by A45, A46, A47, MESFUN6C:def 3; :: thesis:

end;

A48: ( -infty < Integral (M,(lim (Re F))) & Integral (M,(lim (Re F))) < +infty ) by A42, MESFUNC5:96;
A49: ( A is convergent implies A is convergent_to_finite_number ) by A29, A48, MESFUNC5:def 12;
then A50: Re I is convergent by A28, A44, RINFSUP2:15;
hence I is convergent by A41, 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 A51: lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A50, A41, COMSEQ_3:39;
A52: ( 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 A28, A29, A44, A49, RINFSUP2:15;
hence lim I = Integral (M,(lim F)) by A43, A40, A51, A52, MESFUN6C:def 3; :: thesis: