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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

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

for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

let E be Element of S; :: thesis: for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

let P be PartFunc of X,REAL; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) implies ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) )

assume that

A1: E = dom (F . 0) and

A2: E = dom P and

A3: for n being Nat holds F . n is E -measurable and

A4: P is_integrable_on M and

A5: for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ; :: thesis: ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

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

A7: for n being Nat holds

( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;

A8: for x being Element of X

for n being Nat st x in E holds

( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

for n being Nat st x in E holds

|.((Re F) . n).| . x <= P . x ;

then consider A being Real_Sequence such that

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

A16: ( ( for x being Element of X st x in E holds

(Re F) # x is convergent ) implies ( A is convergent & lim A = Integral (M,(lim (Re F))) ) ) by A2, A4, A6, A7, Th48;

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

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

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

reconsider I = I as Complex_Sequence ;

A19: E = dom ((Im F) . 0) by A1, MESFUN7C:def 12;

for x being Element of X

for n being Nat st x in E holds

|.((Im F) . n).| . x <= P . x by A8;

then consider B being Real_Sequence such that

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

A21: ( ( for x being Element of X st x in E holds

(Im F) # x is convergent ) implies ( B is convergent & lim B = Integral (M,(lim (Im F))) ) ) by A2, A4, A19, A7, Th48;

A22: for n being Nat holds

( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M )

(Re I) . x = A . x ;

then A33: Re I = A ;

take I ; :: thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

(Im I) . x = B . x by A26;

then A34: Im I = B ;

for M being sigma_Measure of S

for E being Element of S

for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( 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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

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

for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

let E be Element of S; :: thesis: for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

let P be PartFunc of X,REAL; :: thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

let F be with_the_same_dom Functional_Sequence of X,COMPLEX; :: thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) implies ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) )

assume that

A1: E = dom (F . 0) and

A2: E = dom P and

A3: for n being Nat holds F . n is E -measurable and

A4: P is_integrable_on M and

A5: for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ; :: thesis: ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

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

A7: for n being Nat holds

( (Re F) . n is E -measurable & (Im F) . n is E -measurable ) by A3, Lm2;

A8: for x being Element of X

for n being Nat st x in E holds

( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

proof

then
for x being Element of X
let x be Element of X; :: thesis: for n being Nat st x in E holds

( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

let n be Nat; :: thesis: ( x in E implies ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) )

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

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

then A9: |.((Re (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

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

then A10: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

assume A11: x in E ; :: thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

then |.(F . n).| . x <= P . x by A5;

then |.((F . n) . x).| <= P . x by VALUED_1:18;

then A12: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;

(Im F) # x = Im (F # x) by A1, A11, MESFUN7C:23;

then A13: |.(((Im F) # x) . n1).| <= P . x by A12, A10, XXREAL_0:2;

(Re F) # x = Re (F # x) by A1, A11, MESFUN7C:23;

then |.(((Re F) # x) . n).| <= P . x by A12, A9, XXREAL_0:2;

then A14: |.(((Re F) . n) . x).| <= P . x by SEQFUNC:def 10;

|.(((Im F) . n) . x).| <= P . x by A13, SEQFUNC:def 10;

hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A14, VALUED_1:18; :: thesis: verum

end;( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

let n be Nat; :: thesis: ( x in E implies ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) )

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

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

then A9: |.((Re (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

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

then A10: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;

assume A11: x in E ; :: thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )

then |.(F . n).| . x <= P . x by A5;

then |.((F . n) . x).| <= P . x by VALUED_1:18;

then A12: |.((F # x) . n).| <= P . x by MESFUN7C:def 9;

(Im F) # x = Im (F # x) by A1, A11, MESFUN7C:23;

then A13: |.(((Im F) # x) . n1).| <= P . x by A12, A10, XXREAL_0:2;

(Re F) # x = Re (F # x) by A1, A11, MESFUN7C:23;

then |.(((Re F) # x) . n).| <= P . x by A12, A9, XXREAL_0:2;

then A14: |.(((Re F) . n) . x).| <= P . x by SEQFUNC:def 10;

|.(((Im F) . n) . x).| <= P . x by A13, SEQFUNC:def 10;

hence ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A14, VALUED_1:18; :: thesis: verum

for n being Nat st x in E holds

|.((Re F) . n).| . x <= P . x ;

then consider A being Real_Sequence such that

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

A16: ( ( for x being Element of X st x in E holds

(Re F) # x is convergent ) implies ( A is convergent & lim A = Integral (M,(lim (Re F))) ) ) by A2, A4, A6, A7, Th48;

defpred S

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

A18: for n being Element of NAT holds S

reconsider I = I as Complex_Sequence ;

A19: E = dom ((Im F) . 0) by A1, MESFUN7C:def 12;

for x being Element of X

for n being Nat st x in E holds

|.((Im F) . n).| . x <= P . x by A8;

then consider B being Real_Sequence such that

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

A21: ( ( for x being Element of X st x in E holds

(Im F) # x is convergent ) implies ( B is convergent & lim B = Integral (M,(lim (Im F))) ) ) by A2, A4, A19, A7, Th48;

A22: for n being Nat holds

( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M )

proof

let n be Nat; :: thesis: ( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M )

( dom ((Re F) . n) = E & dom ((Im F) . n) = E ) by A6, A19, MESFUNC8:def 2;

hence ( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M ) by A2, A4, A23, A24, A25, MESFUNC6:96; :: thesis: verum

end;A23: now :: thesis: for x being Element of X st x in dom ((Re F) . n) holds

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

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

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

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

then x in E by A6, MESFUNC8:def 2;

then |.((Re F) . n).| . x <= P . x by A8;

hence |.(((Re F) . n) . x).| <= P . x by VALUED_1:18; :: thesis: verum

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

then x in E by A6, MESFUNC8:def 2;

then |.((Re F) . n).| . x <= P . x by A8;

hence |.(((Re F) . n) . x).| <= P . x by VALUED_1:18; :: thesis: verum

A24: now :: thesis: for x being Element of X st x in dom ((Im F) . n) holds

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

A25:
( (Re F) . n is E -measurable & (Im F) . n is E -measurable )
by A3, Lm2;|.(((Im F) . n) . x).| <= P . x

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

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

then x in E by A19, MESFUNC8:def 2;

then |.((Im F) . n).| . x <= P . x by A8;

hence |.(((Im F) . n) . x).| <= P . x by VALUED_1:18; :: thesis: verum

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

then x in E by A19, MESFUNC8:def 2;

then |.((Im F) . n).| . x <= P . x by A8;

hence |.(((Im F) . n) . x).| <= P . x by VALUED_1:18; :: thesis: verum

( dom ((Re F) . n) = E & dom ((Im F) . n) = E ) by A6, A19, MESFUNC8:def 2;

hence ( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M ) by A2, A4, A23, A24, A25, MESFUNC6:96; :: thesis: verum

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

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

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

let n1 be set ; :: thesis: ( n1 in NAT implies ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 ) )

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

then reconsider n = n1 as Element of NAT ;

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

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

then A29: Im (F . n) is_integrable_on M by A22;

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

then Re (F . n) is_integrable_on M by A22;

then F . n is_integrable_on M by A29, MESFUN6C:def 2;

then consider RF, IF being Real such that

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

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

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

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

hence ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 ) by A15, A20, A30, A28, A31, A27; :: thesis: verum

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

then reconsider n = n1 as Element of NAT ;

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

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

then A29: Im (F . n) is_integrable_on M by A22;

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

then Re (F . n) is_integrable_on M by A22;

then F . n is_integrable_on M by A29, MESFUN6C:def 2;

then consider RF, IF being Real such that

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

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

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

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

hence ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 ) by A15, A20, A30, A28, A31, A27; :: thesis: verum

(Re I) . x = A . x ;

then A33: Re I = A ;

take I ; :: thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

hereby :: thesis: ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) )

for x being object st x in NAT holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) )

let n be Nat; :: thesis: I . n = Integral (M,(F . n))

n is Element of NAT by ORDINAL1:def 12;

hence I . n = Integral (M,(F . n)) by A18; :: thesis: verum

end;n is Element of NAT by ORDINAL1:def 12;

hence I . n = Integral (M,(F . n)) by A18; :: thesis: verum

(Im I) . x = B . x by A26;

then A34: Im I = B ;

hereby :: thesis: verum

assume A35:
for x being Element of X st x in E holds

F # x is convergent ; :: thesis: ( I is convergent & lim I = Integral (M,(lim F)) )

then A36: Integral (M,(lim (Im F))) = Integral (M,(Im (lim F))) by A1, MESFUN7C:25;

A37: ( lim F is_integrable_on M & Integral (M,(lim (Re F))) = Integral (M,(Re (lim F))) ) by A1, A2, A3, A4, A5, A35, Th51, MESFUN7C:25;

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 lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A16, A21, A33, A34, A38, COMSEQ_3:39;

hence lim I = Integral (M,(lim F)) by A16, A21, A33, A34, A38, A37, A36, MESFUN6C:def 3; :: thesis: verum

end;F # x is convergent ; :: thesis: ( I is convergent & lim I = Integral (M,(lim F)) )

then A36: Integral (M,(lim (Im F))) = Integral (M,(Im (lim F))) by A1, MESFUN7C:25;

A37: ( lim F is_integrable_on M & Integral (M,(lim (Re F))) = Integral (M,(Re (lim F))) ) by A1, A2, A3, A4, A5, A35, Th51, MESFUN7C:25;

A38: now :: thesis: for x being Element of X st x in E holds

( (Re F) # x is convergent & (Im F) # x is convergent )

hence
I is convergent
by A16, A21, A33, A34, COMSEQ_3:42; :: thesis: lim I = Integral (M,(lim F))( (Re F) # x is convergent & (Im F) # x is convergent )

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

assume A39: x in E ; :: thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )

F # x is convergent Complex_Sequence by A35, A39;

then ( Re (F # x) is convergent & Im (F # x) is convergent ) ;

hence ( (Re F) # x is convergent & (Im F) # x is convergent ) by A1, A39, MESFUN7C:23; :: thesis: verum

end;assume A39: x in E ; :: thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )

F # x is convergent Complex_Sequence by A35, A39;

then ( Re (F # x) is convergent & Im (F # x) is convergent ) ;

hence ( (Re F) # x is convergent & (Im F) # x is convergent ) by A1, A39, MESFUN7C:23; :: thesis: verum

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 lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A16, A21, A33, A34, A38, COMSEQ_3:39;

hence lim I = Integral (M,(lim F)) by A16, A21, A33, A34, A38, A37, A36, MESFUN6C:def 3; :: thesis: verum