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,REAL
for f being PartFunc of X,REAL 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 ExtREAL_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,REAL
for f being PartFunc of X,REAL 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 ExtREAL_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,REAL
for f being PartFunc of X,REAL 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 ExtREAL_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,REAL
for f being PartFunc of X,REAL 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 ExtREAL_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,REAL ; :: thesis: for f being PartFunc of X,REAL 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 ExtREAL_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,REAL ; :: 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 ExtREAL_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 ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,f ) )
A4: for n being Nat holds (R_EAL F) . n is_integrable_on M

proof

let n be Nat; :: thesis: (R_EAL F) . n is_integrable_on M
F . n is_integrable_on M by A2;
then R_EAL (F . n) is_integrable_on M by MESFUNC6:def 9;
hence (R_EAL F) . n is_integrable_on M ; :: thesis: verum

end;

A5: for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom ((R_EAL F) . 0 ) holds
|.((((R_EAL F) . n) . x) - ((R_EAL 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 set st n >= N & x in dom ((R_EAL F) . 0 ) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e )
assume e > 0 ; :: thesis: ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom ((R_EAL F) . 0 ) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e
then consider N being Nat such that
A6: 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, Def5;

now

let n be Nat; :: thesis: for x being set st n >= N & x in dom ((R_EAL F) . 0 ) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e
let x be set ; :: thesis: ( n >= N & x in dom ((R_EAL F) . 0 ) implies |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e )
assume ( n >= N & x in dom ((R_EAL F) . 0 ) ) ; :: thesis: |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e
then A7: |.(((F . n) . x) - (f . x)).| < e by A6;
|.(((F . n) . x) - (f . x)).| = |.(R_EAL (((F . n) . x) - (f . x))).| by MESFUNC6:43;
hence |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e by A7, SUPINF_2:5; :: thesis: verum

end;

hence ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom ((R_EAL F) . 0 ) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e ; :: thesis: verum

end;

dom ((R_EAL F) . 0 ) = dom (R_EAL f) by A3, Def5;
then A8: R_EAL F is_uniformly_convergent_to R_EAL f by A5, MESFUN10:def 2;
then A9: R_EAL f is_integrable_on M by A1, A4, MESFUN10:22;
consider I being ExtREAL_sequence such that
A10: for n being Nat holds I . n = Integral M,((R_EAL F) . n) and
A11: ( I is convergent & lim I = Integral M,(R_EAL f) ) by A1, A4, A8, MESFUN10:22;
for n being Nat holds I . n = Integral M,(F . n) by A10;
hence ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,f ) ) by A9, A11, MESFUNC6:def 9; :: thesis: verum