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 & E = dom (F . 0 ) ) and
A2: for n being Nat holds F . n is_integrable_on M and
A3: 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 ) )
A4: ( E = dom ((Re F) . 0 ) & E = dom ((Im F) . 0 ) ) by A1, MESFUN7C:def 12, MESFUN7C:def 11;
A5: for n being Nat holds (Re F) . n is_integrable_on M
proof
let n be Nat; :: thesis: (Re F) . n is_integrable_on M
F . n is_integrable_on M by A2;
then Re (F . n) is_integrable_on M by MESFUN6C:def 4;
hence (Re F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum
end;
A6: for n being Nat holds (Im F) . n is_integrable_on M
proof
let n be Nat; :: thesis: (Im F) . n is_integrable_on M
F . n is_integrable_on M by A2;
then Im (F . n) is_integrable_on M by MESFUN6C:def 4;
hence (Im F) . n is_integrable_on M by MESFUN7C:24; :: thesis: verum
end;
A7: ( dom (F . 0 ) = dom f & ( for e being real number 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 (F . 0 ) holds
|.(((F . n) . x) - (f . x)).| < e ) ) by A3, DefUCc;
then ( dom ((Re F) . 0 ) = dom f & dom ((Im F) . 0 ) = dom f ) by MESFUN7C:def 12, MESFUN7C:def 11;
then A8: ( dom ((Re F) . 0 ) = dom (Re f) & dom ((Im F) . 0 ) = dom (Im f) ) by MESFUN6C:def 1, MESFUN6C:def 2;
for e being real number 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
let e be real number ; :: 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
P01: 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 A3, DefUCc;
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
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 Q01: ( n >= N & x in dom ((Re F) . 0 ) ) ; :: thesis: |.((((Re F) . n) . x) - ((Re f) . x)).| < e
then Q02: x in dom (F . 0 ) by MESFUN7C:def 11;
(F . n) . x = (F # x) . n by MESFUN7C:def 9;
then Q05: |.(((F # x) . n) - (f . x)).| < e by P01, Q01, Q02;
f . x in rng f by Q02, A7, FUNCT_1:12;
then Q07: Re (((F # x) . n) - (f . x)) = (Re ((F # x) . n)) - (Re (f . x)) by COMPLEX1:48;
((F # x) . n) - (f . x) is Element of COMPLEX by XCMPLX_0:def 2;
then Q08: |.((Re ((F # x) . n)) - (Re (f . x))).| <= |.(((F # x) . n) - (f . x)).| by Q07, COMSEQ_3:13;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
Q09: Re ((F # x) . n) = (Re (F # x)) . n1 by COMSEQ_3:def 3
.= ((Re F) # x) . n by Q02, MESFUN7C:23
.= ((Re F) . n1) . x by SEQFUNC:def 11 ;
x in dom (Re f) by Q02, A7, MESFUN6C:def 1;
then Re (f . x) = (Re f) . x by MESFUN6C:def 1;
hence |.((((Re F) . n) . x) - ((Re f) . x)).| < e by Q08, Q09, Q05, XXREAL_0:2; :: thesis: verum
end;
hence 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 ; :: thesis: verum
end;
then A9: Re F is_uniformly_convergent_to Re f by A8, DefUCr;
then A10: Re f is_integrable_on M by A1, A4, A5, MES1022r;
for e being real number 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
let e be real number ; :: 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
P01: 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 A3, DefUCc;
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
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 Q01: ( n >= N & x in dom ((Im F) . 0 ) ) ; :: thesis: |.((((Im F) . n) . x) - ((Im f) . x)).| < e
then Q02: x in dom (F . 0 ) by MESFUN7C:def 12;
then |.(((F . n) . x) - (f . x)).| < e by P01, Q01;
then Q05: |.(((F # x) . n) - (f . x)).| < e by MESFUN7C:def 9;
f . x in rng f by Q02, A7, FUNCT_1:12;
then Q07: Im (((F # x) . n) - (f . x)) = (Im ((F # x) . n)) - (Im (f . x)) by COMPLEX1:48;
((F # x) . n) - (f . x) is Element of COMPLEX by XCMPLX_0:def 2;
then Q08: |.((Im ((F # x) . n)) - (Im (f . x))).| <= |.(((F # x) . n) - (f . x)).| by Q07, COMSEQ_3:13;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
Q09: Im ((F # x) . n1) = (Im (F # x)) . n by COMSEQ_3:def 4
.= ((Im F) # x) . n1 by Q02, MESFUN7C:23
.= ((Im F) . n) . x by SEQFUNC:def 11 ;
x in dom (Im f) by Q02, A7, MESFUN6C:def 2;
then Im (f . x) = (Im f) . x by MESFUN6C:def 2;
hence |.((((Im F) . n) . x) - ((Im f) . x)).| < e by Q08, Q09, Q05, XXREAL_0:2; :: thesis: verum
end;
hence 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 ; :: thesis: verum
end;
then A11: Im F is_uniformly_convergent_to Im f by A8, DefUCr;
then A12: Im f is_integrable_on M by A1, A4, A6, MES1022r;
hence A13: f is_integrable_on M by A10, MESFUN6C:def 4; :: 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 )
defpred S1[ Element of NAT , set ] means $2 = Integral M,(F . $1);
A14: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of COMPLEX st S1[n,y]
Integral M,(F . n) is Element of COMPLEX by XCMPLX_0:def 2;
hence ex y being Element of COMPLEX st S1[n,y] ; :: thesis: verum
end;
consider I being Function of NAT ,COMPLEX such that
A15: for n being Element of NAT holds S1[n,I . n] from FUNCT_2:sch 3(A14);
 reconsider I = I as Complex_Sequence ;
take I ; :: thesis: ( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,f )
consider A being ExtREAL_sequence such that
A16: ( ( for n being Nat holds A . n = Integral M,((Re F) . n) ) & A is convergent & lim A = Integral M,(Re f) ) by A1, A4, A5, A9, MES1022r;
consider B being ExtREAL_sequence such that
A17: ( ( for n being Nat holds B . n = Integral M,((Im F) . n) ) & B is convergent & lim B = Integral M,(Im f) ) by A1, A4, A6, A11, MES1022r;
now
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 ;
P03: ( (Re F) . n = Re (F . n) & (Im F) . n = Im (F . n) & (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by MESFUN7C:24, COMSEQ_3:def 3, COMSEQ_3:def 4;
F . n is_integrable_on M by A2;
then consider RF, IF being Real such that
P06: ( RF = Integral M,(Re (F . n)) & IF = Integral M,(Im (F . n)) & Integral M,(F . n) = RF + (IF * <i> ) ) by MESFUN6C:def 5;
I . n1 = Integral M,(F . n) by A15;
then ( Re (I . n1) = RF & Im (I . n1) = IF ) by P06, COMPLEX1:28;
hence ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 ) by A16, A17, P03, P06; :: thesis: verum
end;
then ( ( for x being set st x in NAT holds
(R_EAL (Re I)) . x = A . x ) & ( for x being set st x in NAT holds
(R_EAL (Im I)) . x = B . x ) ) ;
then A18: ( Re I = A & Im I = B ) by FUNCT_2:18;
A19: ( -infty < Integral M,(Re f) & Integral M,(Re f) < +infty & -infty < Integral M,(Im f) & Integral M,(Im f) < +infty ) by A10, A12, MESFUNC6:90;
A20: now
assume R01: A is convergent ; :: thesis: A is convergent_to_finite_number
assume not A is convergent_to_finite_number ; :: thesis: contradiction
then ( A is convergent_to_+infty or A is convergent_to_-infty ) by R01, MESFUNC5:def 11;
hence contradiction by A16, A19, MESFUNC5:def 12; :: thesis: verum
end;
A21: now
assume R01: B is convergent ; :: thesis: B is convergent_to_finite_number
assume not B is convergent_to_finite_number ; :: thesis: contradiction
then ( B is convergent_to_+infty or B is convergent_to_-infty ) by R01, MESFUNC5:def 11;
hence contradiction by A17, A19, MESFUNC5:def 12; :: thesis: verum
end;
then A22: ( lim (Re I) = Integral M,(Re f) & lim (Im I) = Integral M,(Im f) ) by A16, A17, A18, A20, RINFSUP2:15;
thus for n being Nat holds I . n = Integral M,(F . n) :: thesis: ( I is convergent & lim I = Integral M,f )
proof
let n be Nat; :: thesis: I . n = Integral M,(F . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
( (Re I) . n1 = Re (I . n1) & (Im I) . n1 = Im (I . n1) ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
then P02: I . n = ((Re I) . n) + (((Im I) . n) * <i> ) by COMPLEX1:29;
P04: F . n is_integrable_on M by A2;
( (Re F) . n = Re (F . n) & (Im F) . n = Im (F . n) ) by MESFUN7C:24;
then ( (Re I) . n = Integral M,(Re (F . n)) & (Im I) . n = Integral M,(Im (F . n)) ) by A16, A17, A18;
hence I . n = Integral M,(F . n) by P02, P04, MESFUN6C:def 5; :: thesis: verum
end;
A23: ( Re I is convergent & Im I is convergent ) by A16, A17, A18, A20, A21, RINFSUP2:15;
hence I is convergent by COMSEQ_3:42; :: thesis: lim I = Integral M,f
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 lim I = (lim (Re I)) + ((lim (Im I)) * <i> ) by A23, COMSEQ_3:39;
hence lim I = Integral M,f by A13, A22, MESFUN6C:def 5; :: thesis: verum