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) and
A2: E = dom P and
A3: for n being Nat holds F . n is E -measurable and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; :: thesis:
A6: R_EAL P is_integrable_on M by A4;
A7: for x being Element of X
for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x

proof

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
A8: 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 A5, A8; :: thesis:

end;

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

proof

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

end;

now :: thesis:

let x be object ; :: thesis:
assume A10: x in dom P ; :: thesis:
then x in dom |.(F . 0).| by A1, A2, VALUED_1:def 11;
then |.(F . 0).| . x = |.((F . 0) . x).| by VALUED_1:def 11;
then |.((F . 0) . x).| <= P . x by A2, A5, A10;
hence 0 <= P . x by COMPLEX1:46; :: thesis:

end;

then P is nonnegative by MESFUNC6:52;
then consider J being ExtREAL_sequence such that
A11: for n being Nat holds J . n = Integral (M,((R_EAL F) . n)) and
lim_inf J >= Integral (M,(lim_inf (R_EAL F))) and
lim_sup J <= Integral (M,(lim_sup (R_EAL F))) and
A12: ( ( for x being Element of X st x in E holds
(R_EAL F) # x is convergent ) implies ( J is convergent & lim J = Integral (M,(lim (R_EAL F))) ) ) by A1, A2, A9, A6, A7, MESFUN10:17;
A13: Integral (M,(R_EAL P)) < +infty by A6, MESFUNC5:96;
for n being Nat holds |.(J . n).| < +infty

proof

let n be Nat; :: thesis:
A14: ( E = dom ((R_EAL F) . n) & (R_EAL F) . n is E -measurable ) by A1, A9, MESFUNC8:def 2;
|.((R_EAL F) . n).| is_integrable_on M by A1, A2, A9, A6, A7, MESFUN10:16;
then (R_EAL F) . n is_integrable_on M by A14, MESFUNC5:100;
then A15: |.(Integral (M,((R_EAL F) . n))).| <= Integral (M,|.((R_EAL F) . n).|) by MESFUNC5:101;
for x being Element of X st x in dom ((R_EAL F) . n) holds
|.(((R_EAL F) . n) . x).| <= (R_EAL P) . x

proof

let x be Element of X; :: thesis:
assume A16: x in dom ((R_EAL F) . n) ; :: thesis:
then x in E by A1, MESFUNC8:def 2;
then A17: |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A7;
x in dom |.((R_EAL F) . n).| by A16, MESFUNC1:def 10;
hence |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x by A17, MESFUNC1:def 10; :: thesis:

end;

then Integral (M,|.((R_EAL F) . n).|) <= Integral (M,(R_EAL P)) by A2, A6, A14, MESFUNC5:102;
then |.(Integral (M,((R_EAL F) . n))).| <= Integral (M,(R_EAL P)) by A15, XXREAL_0:2;
then |.(Integral (M,((R_EAL F) . n))).| < +infty by A13, XXREAL_0:2;
hence |.(J . n).| < +infty by A11; :: thesis:

end;

then for n being Element of NAT st n in dom J holds
|.(J . n).| < +infty ;
then J is real-valued by MESFUNC2:def 1;
then reconsider I = J as Real_Sequence by RINFSUP2:6;
( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) )

proof

assume A18: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:

A19: now :: thesis:

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

end;

lim F is_integrable_on M by A1, A2, A3, A4, A5, A18, Th47;
then A21: ( -infty < Integral (M,(lim F)) & Integral (M,(lim F)) < +infty ) by MESFUNC5:96;
( J is convergent implies J is convergent_to_finite_number ) by A12, A19, A21, MESFUNC5:def 12;
hence ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) by A12, A19; :: thesis:

end;

then A22: ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) by RINFSUP2:15;
for n being Nat holds I . n = Integral (M,(F . n)) by A11;
hence ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A22; :: thesis: