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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E 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) ) )
B2: for n being Nat holds (R_EAL F) . n is_measurable_on E

proof

let n be Nat; :: thesis: (R_EAL F) . n is_measurable_on E
F . n is_measurable_on E by A2;
then R_EAL (F . n) is_measurable_on E by MESFUNC6:def 6;
hence (R_EAL F) . n is_measurable_on E ; :: thesis: verum

end;

consider K being real number such that
B3: for n being Nat
for x being Element of X st x in dom (F . 0 ) holds
|.((F . n) . x).| <= K by A3, DefUBr;
for n being Nat
for x being set st x in dom ((R_EAL F) . 0 ) holds
|.(((R_EAL F) . n) . x).| <= K

proof

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 )
assume P01: x in dom ((R_EAL F) . 0 ) ; :: thesis: |.(((R_EAL F) . n) . x).| <= K
|.((F . n) . x).| = |.(R_EAL ((F . n) . x)).| by MESFUNC6:43;
hence |.(((R_EAL F) . n) . x).| <= K by P01, B3; :: thesis: verum

end;

then B4: R_EAL F is uniformly_bounded by MESFUN10:def 1;
C0: for x being Element of X st x in E holds
(R_EAL F) # x is convergent

proof

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 P01: F # x is convergent by A4;
(R_EAL F) # x = F # x by MESFUN7C:1;
hence (R_EAL F) # x is convergent by P01, RINFSUP2:14; :: thesis: verum

end;

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,(lim (R_EAL F)) ) by C0, A1, B2, B4, MESFUN10:20;
C3: for n being Nat holds F . n is_integrable_on M

proof

let n be Nat; :: thesis: F . n is_integrable_on M
R_EAL (F . n) is_integrable_on M by C0, A1, B2, B4, MESFUN10:20;
hence F . n is_integrable_on M by MESFUNC6:def 9; :: thesis: verum

end;

for n being Nat holds I . n = Integral M,(F . n) by C2;
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 C2, C3, C0, A1, B2, B4, MESFUN10:20; :: thesis: verum