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, Def7;
A7: 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
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, Def7;
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;
((F # x) . n) - (f . x) is Element of COMPLEX by XCMPLX_0:def 2;
then 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, Def5;
A17: 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
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, Def7;
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;
((F # x) . n) - (f . x) is Element of COMPLEX by XCMPLX_0:def 2;
then 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, Def5;
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 Function of NAT,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
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 set st x in NAT holds
(R_EAL (Im I)) . x = B . x ;
then A46: Im I = B by FUNCT_2:12;
A47: ( -infty < Integral (M,(Im f)) & Integral (M,(Im f)) < +infty ) by A31, MESFUNC6:90;
A48: now
assume A49: 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 A49, MESFUNC5:def 11;
hence contradiction by A39, A40, A47, MESFUNC5:def 12; :: thesis: verum
end;
then A50: lim (Im I) = Integral (M,(Im f)) by A39, A40, A46, RINFSUP2:15;
A51: 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 set st x in NAT holds
(R_EAL (Re I)) . x = A . x by A41;
then A52: Re I = A by FUNCT_2:12;
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 A53: I . n = ((Re I) . n) + (((Im I) . n) * <i>) by COMPLEX1:13;
(Re F) . n = Re (F . n) by MESFUN7C:24;
then A54: (Re I) . n = Integral (M,(Re (F . n))) by A33, A52;
(Im F) . n = Im (F . n) by MESFUN7C:24;
then A55: (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 A53, A54, A55, MESFUN6C:def 3; :: thesis: verum
end;
A56: ( -infty < Integral (M,(Re f)) & Integral (M,(Re f)) < +infty ) by A36, MESFUNC6:90;
A57: now
assume A58: 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 A58, MESFUNC5:def 11;
hence contradiction by A34, A35, A56, MESFUNC5:def 12; :: thesis: verum
end;
then A59: Re I is convergent by A34, A52, RINFSUP2:15;
hence I is convergent by A51, 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 5, COMSEQ_3:def 6;
then A60: lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A59, A51, COMSEQ_3:39;
lim (Re I) = Integral (M,(Re f)) by A34, A35, A52, A57, RINFSUP2:15;
hence lim I = Integral (M,f) by A37, A50, A60, MESFUN6C:def 3; :: thesis: verum