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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim 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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim 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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )

let F be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) ) )

assume that

A1: ( M . E < +infty & E = dom (F . 0) ) and

A2: for n being Nat holds F . n is E -measurable and

A3: F is uniformly_bounded and

A4: for x being Element of X st x in E holds

F # x is convergent ; :: thesis: ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )

consider K being Real such that

A5: for n being Nat

for x being Element of X st x in dom (F . 0) holds

|.((F . n) . x).| <= K by A3;

A6: for x being Element of X st x in E holds

(R_EAL F) # x is convergent

for x being set st x in dom ((R_EAL F) . 0) holds

|.(((R_EAL F) . n) . x).| <= K

A10: for n being Nat holds (R_EAL F) . n is E -measurable

A11: for n being Nat holds I . n = Integral (M,((R_EAL F) . n)) and

A12: ( I is convergent & lim I = Integral (M,(lim (R_EAL F))) ) by A1, A9, A6, MESFUN10:19;

for n being Nat holds I . n = Integral (M,(F . n)) by A11;

hence ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) ) by A1, A10, A9, A6, A12, MESFUN10:19; :: 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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim 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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim 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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )

let E be Element of S; :: thesis: for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )

let F be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) ) )

assume that

A1: ( M . E < +infty & E = dom (F . 0) ) and

A2: for n being Nat holds F . n is E -measurable and

A3: F is uniformly_bounded and

A4: for x being Element of X st x in E holds

F # x is convergent ; :: thesis: ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )

consider K being Real such that

A5: for n being Nat

for x being Element of X st x in dom (F . 0) holds

|.((F . n) . x).| <= K by A3;

A6: for x being Element of X st x in E holds

(R_EAL F) # x is convergent

proof

for n being Nat
let x be Element of X; :: thesis: ( x in E implies (R_EAL F) # x is convergent )

assume x in E ; :: thesis: (R_EAL F) # x is convergent

then A7: F # x is convergent by A4;

(R_EAL F) # x = F # x by MESFUN7C:1;

hence (R_EAL F) # x is convergent by A7, RINFSUP2:14; :: thesis: verum

end;assume x in E ; :: thesis: (R_EAL F) # x is convergent

then A7: F # x is convergent by A4;

(R_EAL F) # x = F # x by MESFUN7C:1;

hence (R_EAL F) # x is convergent by A7, RINFSUP2:14; :: thesis: verum

for x being set st x in dom ((R_EAL F) . 0) holds

|.(((R_EAL F) . n) . x).| <= K

proof

then A9:
R_EAL F is uniformly_bounded
by MESFUN10:def 1;
let n be Nat; :: thesis: for x being set st x in dom ((R_EAL F) . 0) holds

|.(((R_EAL F) . n) . x).| <= K

let x be set ; :: thesis: ( x in dom ((R_EAL F) . 0) implies |.(((R_EAL F) . n) . x).| <= K )

A8: |.((F . n) . x).| = |.((F . n) . x).| by MESFUNC6:43;

assume x in dom ((R_EAL F) . 0) ; :: thesis: |.(((R_EAL F) . n) . x).| <= K

hence |.(((R_EAL F) . n) . x).| <= K by A5, A8; :: thesis: verum

end;|.(((R_EAL F) . n) . x).| <= K

let x be set ; :: thesis: ( x in dom ((R_EAL F) . 0) implies |.(((R_EAL F) . n) . x).| <= K )

A8: |.((F . n) . x).| = |.((F . n) . x).| by MESFUNC6:43;

assume x in dom ((R_EAL F) . 0) ; :: thesis: |.(((R_EAL F) . n) . x).| <= K

hence |.(((R_EAL F) . n) . x).| <= K by A5, A8; :: thesis: verum

A10: for n being Nat holds (R_EAL F) . n is E -measurable

proof

then consider I being ExtREAL_sequence such that
let n be Nat; :: thesis: (R_EAL F) . n is E -measurable

F . n is E -measurable by A2;

then R_EAL (F . n) is E -measurable ;

hence (R_EAL F) . n is E -measurable ; :: thesis: verum

end;F . n is E -measurable by A2;

then R_EAL (F . n) is E -measurable ;

hence (R_EAL F) . n is E -measurable ; :: thesis: verum

A11: for n being Nat holds I . n = Integral (M,((R_EAL F) . n)) and

A12: ( I is convergent & lim I = Integral (M,(lim (R_EAL F))) ) by A1, A9, A6, MESFUN10:19;

for n being Nat holds I . n = Integral (M,(F . n)) by A11;

hence ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) ) by A1, A10, A9, A6, A12, MESFUN10:19; :: thesis: verum