let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let F be with_the_same_dom Functional_Sequence of X,REAL; :: thesis:
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:
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

let x be Element of X; :: thesis:
assume x in E ; :: thesis:
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:

end;

for n being Nat
for x being set st x in dom ((R_EAL F) . 0) holds
|.(((R_EAL F) . n) . x).| <= K

let n be Nat; :: thesis:
let x be set ; :: thesis:
A8: |.((F . n) . x).| = |.((F . n) . x).| by MESFUNC6:43;
assume x in dom ((R_EAL F) . 0) ; :: thesis:
hence |.(((R_EAL F) . n) . x).| <= K by A5, A8; :: thesis:

end;

then A9: R_EAL F is uniformly_bounded by MESFUN10:def 1;
A10: for n being Nat holds (R_EAL F) . n is E -measurable

let n be Nat; :: thesis:
F . n is E -measurable by A2;
then R_EAL (F . n) is E -measurable ;
hence (R_EAL F) . n is E -measurable ; :: thesis:

end;

then consider I being ExtREAL_sequence such that
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: