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
proof
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;
A6: dom (F . 0) = dom f by A4;
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
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
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 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;
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;
dom ((Im F) . 0) = dom f by A6, MESFUN7C:def 12;
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
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
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 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;
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;
dom ((Re F) . 0) = dom f by A6, MESFUN7C:def 11;
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 S1[ Element of NAT , set ] means $2 = Integral (M,(F . $1));
A27: 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 sequence of COMPLEX such that
A28: for n being Element of NAT holds S1[n,I . n] from FUNCT_2:sch 3(A27);
 A29: 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 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;
A30: E = dom ((Im F) . 0) by A2, MESFUN7C:def 12;
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 )
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;
then for x being object st x in NAT holds
(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
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;
A55: ( -infty < Integral (M,(Re f)) & Integral (M,(Re f)) < +infty ) by A36, MESFUNC6:90;
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