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

let n be Nat; :: thesis:
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:

end;

B3: R_EAL P is_integrable_on M by A3, MESFUNC6:def 9;
B4: for x being Element of X
for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x

end;

let x be Element of X; :: thesis:
assume x in E ; :: thesis:
then P01: F # x is convergent by A5;
(R_EAL F) # x = F # x by MESFUN7C:1;
hence (R_EAL F) # x is convergent by P01, RINFSUP2:14; :: thesis:

end;

hence lim F is_integrable_on M by A1, B2, B3, B4, MES1017e; :: thesis: