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_measurable_on E 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, MESFUNC6:def 9;
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_measurable_on E

proof

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

end;

now

let x be set ; :: 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:132; :: 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:18;
A13: Integral M,(R_EAL P) < +infty by A6, MESFUNC5:102;
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_measurable_on E ) by A1, A9, MESFUNC8:def 2;
|.((R_EAL F) . n).| is_integrable_on M by A1, A2, A9, A6, A7, MESFUN10:17;
then (R_EAL F) . n is_integrable_on M by A14, MESFUNC5:106;
then A15: |.(Integral M,((R_EAL F) . n)).| <= Integral M,|.((R_EAL F) . n).| by MESFUNC5:107;
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:108;
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 V44() 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

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:102;

now

assume A22: J is convergent ; :: thesis:
assume not J is convergent_to_finite_number ; :: thesis:
then ( J is convergent_to_+infty or J is convergent_to_-infty ) by A22, MESFUNC5:def 11;
hence contradiction by A12, A19, A21, MESFUNC5:def 12; :: thesis:

end;

hence ( J is convergent_to_finite_number & lim J = Integral M,(lim F) ) by A12, A19; :: thesis:

end;

then A23: ( ( 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 A23; :: thesis: