let X be non empty set ; :: thesis:
let F be with_the_same_dom Functional_Sequence of X,ExtREAL ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
assume that
A1: ( M . E < +infty & E = dom (F . 0 ) ) and
A2: for n being Nat holds F . n is_measurable_on E 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 K1 being real number such that
A5: for n being Nat
for x being set st x in dom (F . 0 ) holds
|.((F . n) . x).| <= K1 by A3, DefUB;
set K = max K1,1;
X: max K1,1 > 0 by XXREAL_0:30;
Y: max K1,1 >= K1 by XXREAL_0:25;
X5: for n being Nat
for x being set st x in dom (F . 0 ) holds
|.((F . n) . x).| <= max K1,1

proof

let n be Nat; :: thesis:
let x be set ; :: thesis:
assume x in dom (F . 0 ) ; :: thesis:
then |.((F . n) . x).| <= K1 by A5;
hence |.((F . n) . x).| <= max K1,1 by Y, XXREAL_0:2; :: thesis:

end;

max K1,1 in REAL by XREAL_0:def 1;
then consider h being PartFunc of X,ExtREAL such that
B1: ( h is_simple_func_in S & dom h = E & ( for x being set st x in E holds
h . x = max K1,1 ) ) by MESFUNC5:47, NUMBERS:31;
for x being set st x in E holds
h . x >= 0. by B1, X;
then B2: h is nonnegative by B1, SUPINF_2:71;
B3: h is_measurable_on E by B1, MESFUNC2:37;
max K1,1 is Real by XREAL_0:def 1;
then B4: integral' M,h = (R_EAL (max K1,1)) * (M . (dom h)) by B1, X, MESFUNC5:110;
B5: (R_EAL (max K1,1)) * +infty = +infty by X, XXREAL_3:def 5;
B6: dom h = dom |.h.| by MESFUNC1:def 10;
B7: for x being Element of X st x in dom h holds
h . x = |.h.| . x

proof

let x be Element of X; :: thesis:
assume x in dom h ; :: thesis:
then B71: x in dom |.h.| by MESFUNC1:def 10;
0 <= h . x by B2, SUPINF_2:70;
then |.(h . x).| = h . x by EXTREAL1:def 3;
hence h . x = |.h.| . x by B71, MESFUNC1:def 10; :: thesis:

end;

B8: ( dom (max+ h) = dom h & dom (max- h) = dom h ) by MESFUNC2:def 2, MESFUNC2:def 3;
B9: ( max+ h is_measurable_on E & max- h is_measurable_on E ) by B1, B3, MESFUNC2:27, MESFUNC2:28;
( ( for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x ) & ( for x being set st x in dom (max- h) holds
0. <= (max- h) . x ) ) by MESFUNC2:14, MESFUNC2:15;
then C1: ( max+ h is nonnegative & max- h is nonnegative ) by SUPINF_2:71;
then C2: dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by MESFUNC5:28;
C3: ( 0 <= integral+ M,(max+ h) & 0 <= integral+ M,(max- h) ) by B1, B8, B9, C1, MESFUNC5:85;
C4: ex C being Element of S st
( C = dom ((max+ h) + (max- h)) & integral+ M,((max+ h) + (max- h)) = (integral+ M,((max+ h) | C)) + (integral+ M,((max- h) | C)) ) by B1, B8, B9, C1, MESFUNC5:84;
C5: ( (max+ h) | E = max+ h & (max- h) | E = max- h ) by B1, B8, RELAT_1:97;
( Integral M,h = integral+ M,h & Integral M,h = integral' M,h ) by B1, B2, MESFUNC5:95;
then integral+ M,h < +infty by B5, B4, B1, A1, X, XXREAL_3:83;
then integral+ M,|.h.| < +infty by B7, B6, PARTFUN1:34;
then (integral+ M,(max+ h)) + (integral+ M,(max- h)) < +infty by C5, C2, B1, B8, C4, MESFUNC2:26;
then ( integral+ M,(max+ h) <> +infty & integral+ M,(max- h) <> +infty ) by C3, XXREAL_3:def 2;
then ( integral+ M,(max+ h) < +infty & integral+ M,(max- h) < +infty ) by XXREAL_0:4;
then C6: h is_integrable_on M by B1, B3, MESFUNC5:def 17;
C7: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= h . x

proof

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
assume C71: x in E ; :: thesis:
then C72: |.((F . n) . x).| <= max K1,1 by A1, X5;
dom (F . n) = dom |.(F . n).| by MESFUNC1:def 10;
then x in dom |.(F . n).| by C71, A1, MESFUNC8:def 2;
then |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def 10;
hence |.(F . n).| . x <= h . x by C72, C71, B1; :: thesis:

end;

E1: now

let n be Nat; :: thesis:
( |.(F . n).| is_integrable_on M & E = dom (F . n) & F . n is_measurable_on E ) by A1, A2, B1, B2, C6, C7, Th136z, MESFUNC8:def 2;
hence F . n is_integrable_on M by MESFUNC5:106; :: thesis:

end;

E4: ( dom (lim_inf F) = dom (F . 0 ) & dom (lim F) = dom (F . 0 ) ) by MESFUNC8:def 8, MESFUNC8:def 10;
for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_inf F) . x

proof

let x be Element of X; :: thesis:
assume E41: x in dom (lim F) ; :: thesis:
then x in E by A1, MESFUNC8:def 10;
then F # x is convergent by A4;
hence (lim F) . x = (lim_inf F) . x by E41, MESFUNC8:14; :: thesis:

end;

then E2: lim F = lim_inf F by E4, PARTFUN1:34;
then E3: lim F is_measurable_on E by A1, A2, MESFUNC8:24;
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & lim_inf I >= Integral M,(lim_inf F) & lim_sup I <= Integral M,(lim_sup F) & ( ( 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 A1, A2, B1, B2, C6, C7, Th136x;
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 A4, E1, E2, E3, A1, E4, D1, MESFUNC5:106; :: thesis: