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

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,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

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,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

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,f) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,f) ) )

let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,f) ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f implies ( 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,f) ) ) )

assume that

A1: M . E < +infty and

A2: E = dom (F . 0) and

A3: for n being Nat holds F . n is_integrable_on M and

A4: F is_uniformly_convergent_to f ; :: thesis: ( 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,f) ) )

A5: for n being Nat holds (Im F) . n is_integrable_on M

A7: for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

then dom ((Im F) . 0) = dom (Im f) by COMSEQ_3:def 4;

then A16: Im F is_uniformly_convergent_to Im f by A7;

A17: for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

then dom ((Re F) . 0) = dom (Re f) by COMSEQ_3:def 3;

then A26: Re F is_uniformly_convergent_to Re f by A17;

defpred S_{1}[ Element of NAT , set ] means $2 = Integral (M,(F . $1));

A27: for n being Element of NAT ex y being Element of COMPLEX st S_{1}[n,y]

A28: for n being Element of NAT holds S_{1}[n,I . n]
from FUNCT_2:sch 3(A27);

A29: for n being Nat holds (Re F) . n is_integrable_on M

then A31: Im f is_integrable_on M by A1, A5, A16, Th50;

A32: E = dom ((Re F) . 0) by A2, MESFUN7C:def 11;

then consider A being ExtREAL_sequence such that

A33: for n being Nat holds A . n = Integral (M,((Re F) . n)) and

A34: A is convergent and

A35: lim A = Integral (M,(Re f)) by A1, A29, A26, Th50;

A36: Re f is_integrable_on M by A1, A32, A29, A26, Th50;

hence A37: f is_integrable_on M by A31, 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,f) )

reconsider I = I as Complex_Sequence ;

consider B being ExtREAL_sequence such that

A38: for n being Nat holds B . n = Integral (M,((Im F) . n)) and

A39: B is convergent and

A40: lim B = Integral (M,(Im f)) by A1, A30, A5, A16, Th50;

(R_EAL (Im I)) . x = B . x ;

then A46: Im I = B ;

A47: ( -infty < Integral (M,(Im f)) & Integral (M,(Im f)) < +infty ) by A31, MESFUNC6:90;

A48: ( B is convergent implies B is convergent_to_finite_number ) by A40, A47, MESFUNC5:def 12;

then A49: lim (Im I) = Integral (M,(Im f)) by A39, A40, A46, RINFSUP2:15;

A50: Im I is convergent by A39, A46, A48, RINFSUP2:15;

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

for x being object st x in NAT holds

(R_EAL (Re I)) . x = A . x by A41;

then A51: Re I = A ;

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

A56: ( A is convergent implies A is convergent_to_finite_number ) by A35, A55, MESFUNC5:def 12;

then A57: Re I is convergent by A34, A51, RINFSUP2:15;

hence I is convergent by A50, COMSEQ_3:42; :: thesis: lim I = Integral (M,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 A58: lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A57, A50, COMSEQ_3:39;

lim (Re I) = Integral (M,(Re f)) by A34, A35, A51, A56, RINFSUP2:15;

hence lim I = Integral (M,f) by A37, A49, A58, 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

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,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

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,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

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,f) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,f) ) )

let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( 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,f) ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f implies ( 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,f) ) ) )

assume that

A1: M . E < +infty and

A2: E = dom (F . 0) and

A3: for n being Nat holds F . n is_integrable_on M and

A4: F is_uniformly_convergent_to f ; :: thesis: ( 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,f) ) )

A5: for n being Nat holds (Im F) . n is_integrable_on M

proof

A6:
dom (F . 0) = dom f
by A4;
let n be Nat; :: thesis: (Im F) . n is_integrable_on M

F . n is_integrable_on M by A3;

then Im (F . n) is_integrable_on M by MESFUN6C:def 2;

hence (Im F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum

end;F . n is_integrable_on M by A3;

then Im (F . n) is_integrable_on M by MESFUN6C:def 2;

hence (Im F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum

A7: for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

proof

dom ((Im F) . 0) = dom f
by A6, MESFUN7C:def 12;
let e be Real; :: thesis: ( e > 0 implies ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e )

assume e > 0 ; :: thesis: ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

then consider N being Nat such that

A8: for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e by A4;

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e ; :: thesis: verum

end;for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e )

assume e > 0 ; :: thesis: ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

then consider N being Nat such that

A8: for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e by A4;

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

proof

hence
ex N being Nat st
let n be Nat; :: thesis: for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e

let x be Element of X; :: thesis: ( n >= N & x in dom ((Im F) . 0) implies |.((((Im F) . n) . x) - ((Im f) . x)).| < e )

assume that

A9: n >= N and

A10: x in dom ((Im F) . 0) ; :: thesis: |.((((Im F) . n) . x) - ((Im f) . x)).| < e

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A11: x in dom (F . 0) by A10, MESFUN7C:def 12;

then |.(((F . n) . x) - (f . x)).| < e by A8, A9;

then A12: |.(((F # x) . n) - (f . x)).| < e by MESFUN7C:def 9;

A13: Im (((F # x) . n) - (f . x)) = (Im ((F # x) . n)) - (Im (f . x)) by COMPLEX1:19;

A14: |.((Im ((F # x) . n)) - (Im (f . x))).| <= |.(((F # x) . n) - (f . x)).| by A13, COMSEQ_3:13;

x in dom (Im f) by A6, A11, COMSEQ_3:def 4;

then A15: Im (f . x) = (Im f) . x by COMSEQ_3:def 4;

Im ((F # x) . n1) = (Im (F # x)) . n by COMSEQ_3:def 6

.= ((Im F) # x) . n1 by A11, MESFUN7C:23

.= ((Im F) . n) . x by SEQFUNC:def 10 ;

hence |.((((Im F) . n) . x) - ((Im f) . x)).| < e by A12, A14, A15, XXREAL_0:2; :: thesis: verum

end;|.((((Im F) . n) . x) - ((Im f) . x)).| < e

let x be Element of X; :: thesis: ( n >= N & x in dom ((Im F) . 0) implies |.((((Im F) . n) . x) - ((Im f) . x)).| < e )

assume that

A9: n >= N and

A10: x in dom ((Im F) . 0) ; :: thesis: |.((((Im F) . n) . x) - ((Im f) . x)).| < e

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A11: x in dom (F . 0) by A10, MESFUN7C:def 12;

then |.(((F . n) . x) - (f . x)).| < e by A8, A9;

then A12: |.(((F # x) . n) - (f . x)).| < e by MESFUN7C:def 9;

A13: Im (((F # x) . n) - (f . x)) = (Im ((F # x) . n)) - (Im (f . x)) by COMPLEX1:19;

A14: |.((Im ((F # x) . n)) - (Im (f . x))).| <= |.(((F # x) . n) - (f . x)).| by A13, COMSEQ_3:13;

x in dom (Im f) by A6, A11, COMSEQ_3:def 4;

then A15: Im (f . x) = (Im f) . x by COMSEQ_3:def 4;

Im ((F # x) . n1) = (Im (F # x)) . n by COMSEQ_3:def 6

.= ((Im F) # x) . n1 by A11, MESFUN7C:23

.= ((Im F) . n) . x by SEQFUNC:def 10 ;

hence |.((((Im F) . n) . x) - ((Im f) . x)).| < e by A12, A14, A15, XXREAL_0:2; :: thesis: verum

for n being Nat

for x being Element of X st n >= N & x in dom ((Im F) . 0) holds

|.((((Im F) . n) . x) - ((Im f) . x)).| < e ; :: thesis: verum

then dom ((Im F) . 0) = dom (Im f) by COMSEQ_3:def 4;

then A16: Im F is_uniformly_convergent_to Im f by A7;

A17: for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

proof

dom ((Re F) . 0) = dom f
by A6, MESFUN7C:def 11;
let e be Real; :: thesis: ( e > 0 implies ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e )

assume e > 0 ; :: thesis: ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

then consider N being Nat such that

A18: for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e by A4;

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e ; :: thesis: verum

end;for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e )

assume e > 0 ; :: thesis: ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

then consider N being Nat such that

A18: for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e by A4;

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

proof

hence
ex N being Nat st
let n be Nat; :: thesis: for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e

let x be Element of X; :: thesis: ( n >= N & x in dom ((Re F) . 0) implies |.((((Re F) . n) . x) - ((Re f) . x)).| < e )

assume that

A19: n >= N and

A20: x in dom ((Re F) . 0) ; :: thesis: |.((((Re F) . n) . x) - ((Re f) . x)).| < e

A21: x in dom (F . 0) by A20, MESFUN7C:def 11;

A22: Re (((F # x) . n) - (f . x)) = (Re ((F # x) . n)) - (Re (f . x)) by COMPLEX1:19;

(F . n) . x = (F # x) . n by MESFUN7C:def 9;

then A23: |.(((F # x) . n) - (f . x)).| < e by A18, A19, A21;

x in dom (Re f) by A6, A21, COMSEQ_3:def 3;

then A24: Re (f . x) = (Re f) . x by COMSEQ_3:def 3;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A25: |.((Re ((F # x) . n)) - (Re (f . x))).| <= |.(((F # x) . n) - (f . x)).| by A22, COMSEQ_3:13;

Re ((F # x) . n) = (Re (F # x)) . n1 by COMSEQ_3:def 5

.= ((Re F) # x) . n by A21, MESFUN7C:23

.= ((Re F) . n1) . x by SEQFUNC:def 10 ;

hence |.((((Re F) . n) . x) - ((Re f) . x)).| < e by A23, A25, A24, XXREAL_0:2; :: thesis: verum

end;|.((((Re F) . n) . x) - ((Re f) . x)).| < e

let x be Element of X; :: thesis: ( n >= N & x in dom ((Re F) . 0) implies |.((((Re F) . n) . x) - ((Re f) . x)).| < e )

assume that

A19: n >= N and

A20: x in dom ((Re F) . 0) ; :: thesis: |.((((Re F) . n) . x) - ((Re f) . x)).| < e

A21: x in dom (F . 0) by A20, MESFUN7C:def 11;

A22: Re (((F # x) . n) - (f . x)) = (Re ((F # x) . n)) - (Re (f . x)) by COMPLEX1:19;

(F . n) . x = (F # x) . n by MESFUN7C:def 9;

then A23: |.(((F # x) . n) - (f . x)).| < e by A18, A19, A21;

x in dom (Re f) by A6, A21, COMSEQ_3:def 3;

then A24: Re (f . x) = (Re f) . x by COMSEQ_3:def 3;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A25: |.((Re ((F # x) . n)) - (Re (f . x))).| <= |.(((F # x) . n) - (f . x)).| by A22, COMSEQ_3:13;

Re ((F # x) . n) = (Re (F # x)) . n1 by COMSEQ_3:def 5

.= ((Re F) # x) . n by A21, MESFUN7C:23

.= ((Re F) . n1) . x by SEQFUNC:def 10 ;

hence |.((((Re F) . n) . x) - ((Re f) . x)).| < e by A23, A25, A24, XXREAL_0:2; :: thesis: verum

for n being Nat

for x being Element of X st n >= N & x in dom ((Re F) . 0) holds

|.((((Re F) . n) . x) - ((Re f) . x)).| < e ; :: thesis: verum

then dom ((Re F) . 0) = dom (Re f) by COMSEQ_3:def 3;

then A26: Re F is_uniformly_convergent_to Re f by A17;

defpred S

A27: 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]

Integral (M,(F . n)) is Element of COMPLEX by XCMPLX_0:def 2;

hence ex y being Element of COMPLEX st S_{1}[n,y]
; :: thesis: verum

end;Integral (M,(F . n)) is Element of COMPLEX by XCMPLX_0:def 2;

hence ex y being Element of COMPLEX st S

A28: for n being Element of NAT holds S

A29: for n being Nat holds (Re F) . n is_integrable_on M

proof

A30:
E = dom ((Im F) . 0)
by A2, MESFUN7C:def 12;
let n be Nat; :: thesis: (Re F) . n is_integrable_on M

F . n is_integrable_on M by A3;

then Re (F . n) is_integrable_on M by MESFUN6C:def 2;

hence (Re F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum

end;F . n is_integrable_on M by A3;

then Re (F . n) is_integrable_on M by MESFUN6C:def 2;

hence (Re F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum

then A31: Im f is_integrable_on M by A1, A5, A16, Th50;

A32: E = dom ((Re F) . 0) by A2, MESFUN7C:def 11;

then consider A being ExtREAL_sequence such that

A33: for n being Nat holds A . n = Integral (M,((Re F) . n)) and

A34: A is convergent and

A35: lim A = Integral (M,(Re f)) by A1, A29, A26, Th50;

A36: Re f is_integrable_on M by A1, A32, A29, A26, Th50;

hence A37: f is_integrable_on M by A31, 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,f) )

reconsider I = I as Complex_Sequence ;

consider B being ExtREAL_sequence such that

A38: for n being Nat holds B . n = Integral (M,((Im F) . n)) and

A39: B is convergent and

A40: lim B = Integral (M,(Im f)) by A1, A30, A5, A16, Th50;

A41: now :: thesis: for n1 being set st n1 in NAT holds

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

then
for x being object st x in NAT holds ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )

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 ;

A42: ( (Re F) . n = Re (F . n) & (Im F) . n = Im (F . n) ) by MESFUN7C:24;

F . n is_integrable_on M by A3;

then consider RF, IF being Real such that

A43: ( RF = Integral (M,(Re (F . n))) & IF = Integral (M,(Im (F . n))) ) and

A44: Integral (M,(F . n)) = RF + (IF * <i>) by MESFUN6C:def 3;

A45: ( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;

I . n1 = Integral (M,(F . n)) by A28;

then ( Re (I . n1) = RF & Im (I . n1) = IF ) by A44, COMPLEX1:12;

hence ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 ) by A33, A38, A42, A45, A43; :: 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 ;

A42: ( (Re F) . n = Re (F . n) & (Im F) . n = Im (F . n) ) by MESFUN7C:24;

F . n is_integrable_on M by A3;

then consider RF, IF being Real such that

A43: ( RF = Integral (M,(Re (F . n))) & IF = Integral (M,(Im (F . n))) ) and

A44: Integral (M,(F . n)) = RF + (IF * <i>) by MESFUN6C:def 3;

A45: ( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;

I . n1 = Integral (M,(F . n)) by A28;

then ( Re (I . n1) = RF & Im (I . n1) = IF ) by A44, COMPLEX1:12;

hence ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 ) by A33, A38, A42, A45, A43; :: thesis: verum

(R_EAL (Im I)) . x = B . x ;

then A46: Im I = B ;

A47: ( -infty < Integral (M,(Im f)) & Integral (M,(Im f)) < +infty ) by A31, MESFUNC6:90;

A48: ( B is convergent implies B is convergent_to_finite_number ) by A40, A47, MESFUNC5:def 12;

then A49: lim (Im I) = Integral (M,(Im f)) by A39, A40, A46, RINFSUP2:15;

A50: Im I is convergent by A39, A46, A48, RINFSUP2:15;

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

for x being object st x in NAT holds

(R_EAL (Re I)) . x = A . x by A41;

then A51: Re I = A ;

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

proof

A55:
( -infty < Integral (M,(Re f)) & Integral (M,(Re f)) < +infty )
by A36, MESFUNC6:90;
let n be Nat; :: thesis: I . n = Integral (M,(F . n))

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

( (Re I) . n1 = Re (I . n1) & (Im I) . n1 = Im (I . n1) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;

then A52: I . n = ((Re I) . n) + (((Im I) . n) * <i>) by COMPLEX1:13;

(Re F) . n = Re (F . n) by MESFUN7C:24;

then A53: (Re I) . n = Integral (M,(Re (F . n))) by A33, A51;

(Im F) . n = Im (F . n) by MESFUN7C:24;

then A54: (Im I) . n = Integral (M,(Im (F . n))) by A38, A46;

F . n is_integrable_on M by A3;

hence I . n = Integral (M,(F . n)) by A52, A53, A54, MESFUN6C:def 3; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

( (Re I) . n1 = Re (I . n1) & (Im I) . n1 = Im (I . n1) ) by COMSEQ_3:def 5, COMSEQ_3:def 6;

then A52: I . n = ((Re I) . n) + (((Im I) . n) * <i>) by COMPLEX1:13;

(Re F) . n = Re (F . n) by MESFUN7C:24;

then A53: (Re I) . n = Integral (M,(Re (F . n))) by A33, A51;

(Im F) . n = Im (F . n) by MESFUN7C:24;

then A54: (Im I) . n = Integral (M,(Im (F . n))) by A38, A46;

F . n is_integrable_on M by A3;

hence I . n = Integral (M,(F . n)) by A52, A53, A54, MESFUN6C:def 3; :: thesis: verum

A56: ( A is convergent implies A is convergent_to_finite_number ) by A35, A55, MESFUNC5:def 12;

then A57: Re I is convergent by A34, A51, RINFSUP2:15;

hence I is convergent by A50, COMSEQ_3:42; :: thesis: lim I = Integral (M,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 A58: lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A57, A50, COMSEQ_3:39;

lim (Re I) = Integral (M,(Re f)) by A34, A35, A51, A56, RINFSUP2:15;

hence lim I = Integral (M,f) by A37, A49, A58, MESFUN6C:def 3; :: thesis: verum