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

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 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

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

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

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

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

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;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

hence
ex N being Nat st 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;|.((((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

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

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