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 ;
hence (R_EAL F) . n is_integrable_on M ; :: thesis: verum

end;

A5: for e being Real 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; :: 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;

now :: thesis: 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

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)).| = |.(((F . n) . x) - (f . x)).| by MESFUNC6:43;
hence |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e by A7; :: 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;
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:21;
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:21;
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; :: thesis: verum