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:
let P be PartFunc of X,REAL; :: thesis:
assume that
A1: ( E = dom (F . 0) & E = dom P ) and
A2: for n being Nat holds F . n is E -measurable and
A3: P is_integrable_on M and
A4: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A5: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
A6: 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;

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

end;

A9: for x being Element of X
for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
A10: R_EAL |.(F . n).| = |.(R_EAL (F . n)).| by MESFUNC6:1;
assume x in E ; :: thesis:
hence |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A4, A10; :: thesis:

end;

R_EAL P is_integrable_on M by A3;
hence lim F is_integrable_on M by A1, A6, A9, A7, Th46; :: thesis: