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 ) )
B3: dom ((R_EAL F) . 0 ) = dom (R_EAL f) by A3, DefUCr;
B2: 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;

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
P1: 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, DefUCr;

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 P2: |.(((F . n) . x) - (f . x)).| < e by P1;
|.(((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 P2, 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;

then C0: R_EAL F is_uniformly_convergent_to R_EAL f by B3, MESFUN10:def 2;
then C1: R_EAL f is_integrable_on M by A1, B2, MESFUN10:22;
consider I being ExtREAL_sequence such that
C2: ( ( for n being Nat holds I . n = Integral M,((R_EAL F) . n) ) & I is convergent & lim I = Integral M,(R_EAL f) ) by C0, A1, B2, MESFUN10:22;
for n being Nat holds I . n = Integral M,(F . n) by C2;
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 C2, C1, MESFUNC6:def 9; :: thesis: verum