let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let M be sigma_Measure of S; :: thesis: for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) )

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: ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

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

for x being Element of X st x in dom ((Im F) . 0) holds

|.(((Im F) . n) . x).| <= K

A12: for x being Element of X st x in E holds

(Im F) # x is convergent_{1}[ 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_{1}[n,y]

A15: for n being Element of NAT holds S_{1}[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

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: ( lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

(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: ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )

take I ; :: thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )

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: ( I is convergent & lim I = Integral (M,(lim F)) )

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: lim I = Integral (M,(lim F))

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: verum

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let M be sigma_Measure of S; :: thesis: for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) )

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: ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

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

proof

for n being Nat
let x be Element of X; :: thesis: ( x in E implies (Re F) # x is convergent )

assume A8: x in E ; :: thesis: (Re F) # x is convergent

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: verum

end;assume A8: x in E ; :: thesis: (Re F) # x is convergent

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: verum

for x being Element of X st x in dom ((Im F) . 0) holds

|.(((Im F) . n) . x).| <= K

proof

then A11:
Im F is uniformly_bounded
;
let n be Nat; :: thesis: for x being Element of X st x in dom ((Im F) . 0) holds

|.(((Im F) . n) . x).| <= K

let x be Element of X; :: thesis: ( x in dom ((Im F) . 0) implies |.(((Im F) . n) . x).| <= K )

assume x in dom ((Im F) . 0) ; :: thesis: |.(((Im F) . n) . x).| <= K

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: verum

end;|.(((Im F) . n) . x).| <= K

let x be Element of X; :: thesis: ( x in dom ((Im F) . 0) implies |.(((Im F) . n) . x).| <= K )

assume x in dom ((Im F) . 0) ; :: thesis: |.(((Im F) . n) . x).| <= K

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: verum

A12: for x being Element of X st x in E holds

(Im F) # x is convergent

proof

defpred S
let x be Element of X; :: thesis: ( x in E implies (Im F) # x is convergent )

assume A13: x in E ; :: thesis: (Im F) # x is convergent

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: verum

end;assume A13: x in E ; :: thesis: (Im F) # x is convergent

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: verum

A14: for n being Element of NAT ex y being Element of COMPLEX st S

proof

consider I being sequence of COMPLEX such that
let n be Element of NAT ; :: thesis: ex y being Element of COMPLEX st S_{1}[n,y]

take Integral (M,(F . n)) ; :: thesis: ( Integral (M,(F . n)) is set & Integral (M,(F . n)) is Element of COMPLEX & S_{1}[n, Integral (M,(F . n))] )

thus ( Integral (M,(F . n)) is set & Integral (M,(F . n)) is Element of COMPLEX & S_{1}[n, Integral (M,(F . n))] )
by XCMPLX_0:def 2, TARSKI:1; :: thesis: verum

end;take Integral (M,(F . n)) ; :: thesis: ( Integral (M,(F . n)) is set & Integral (M,(F . n)) is Element of COMPLEX & S

thus ( Integral (M,(F . n)) is set & Integral (M,(F . n)) is Element of COMPLEX & S

A15: for n being Element of NAT holds S

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

proof

then A19:
Re F is uniformly_bounded
;
let n be Nat; :: thesis: for x being Element of X st x in dom ((Re F) . 0) holds

|.(((Re F) . n) . x).| <= K

let x be Element of X; :: thesis: ( x in dom ((Re F) . 0) implies |.(((Re F) . n) . x).| <= K )

assume x in dom ((Re F) . 0) ; :: thesis: |.(((Re F) . n) . x).| <= K

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: verum

end;|.(((Re F) . n) . x).| <= K

let x be Element of X; :: thesis: ( x in dom ((Re F) . 0) implies |.(((Re F) . n) . x).| <= K )

assume x in dom ((Re F) . 0) ; :: thesis: |.(((Re F) . n) . x).| <= K

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: verum

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: ( lim F is_integrable_on M & ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )

proof

A32:
for n1 being set st n1 in NAT holds
let n be Nat; :: thesis: F . n is_integrable_on M

(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: verum

end;(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: verum

( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

proof

then
for n1 being object st n1 in NAT holds
let n1 be set ; :: thesis: ( n1 in NAT implies ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 ) )

assume n1 in NAT ; :: thesis: ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

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: (R_EAL (Im I)) . n1 = B . n1

(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: verum

end;assume n1 in NAT ; :: thesis: ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

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: (R_EAL (Im I)) . n1 = B . n1

(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: verum

(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: ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )

take I ; :: thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )

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: ( I is convergent & lim I = Integral (M,(lim F)) )

proof

A48:
( -infty < Integral (M,(lim (Re F))) & Integral (M,(lim (Re F))) < +infty )
by A42, MESFUNC5:96;
let n be Nat; :: thesis: I . n = Integral (M,(F . n))

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: verum

end;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: verum

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: lim I = Integral (M,(lim F))

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: verum