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 and
A2: E = dom (F . 0 ) and
A3: for n being Nat holds F . n is_measurable_on E and
A4: F is uniformly_bounded and
A5: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
consider K1 being real number such that
A6: for n being Nat
for x being set st x in dom (F . 0 ) holds
|.((F . n) . x).| <= K1 by A4, Def1;
set K = max K1,1;
max K1,1 in REAL by XREAL_0:def 1;
then consider h being PartFunc of X,ExtREAL such that
A7: h is_simple_func_in S and
A8: dom h = E and
A9: for x being set st x in E holds
h . x = max K1,1 by MESFUNC5:47, NUMBERS:31;
A10: dom h = dom |.h.| by MESFUNC1:def 10;
A11: max K1,1 > 0 by XXREAL_0:30;
then A12: (R_EAL (max K1,1)) * +infty = +infty by XXREAL_3:def 5;
for x being set st x in E holds
h . x >= 0. by A11, A9;
then A13: h is nonnegative by A8, SUPINF_2:71;
then A14: Integral M,h = integral' M,h by A7, MESFUNC5:95;
max K1,1 is Real by XREAL_0:def 1;
then A15: integral' M,h = (R_EAL (max K1,1)) * (M . (dom h)) by A11, A8, A9, MESFUNC5:110;
A16: 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 A17: x in dom |.h.| by MESFUNC1:def 10;
0 <= h . x by A13, SUPINF_2:70;
then |.(h . x).| = h . x by EXTREAL1:def 3;
hence h . x = |.h.| . x by A17, MESFUNC1:def 10; :: thesis:

end;

Integral M,h = integral+ M,h by A7, A13, MESFUNC5:95;
then integral+ M,h < +infty by A1, A11, A8, A15, A12, A14, XXREAL_3:83;
then A18: integral+ M,|.h.| < +infty by A10, A16, PARTFUN1:34;
A19: dom (max+ h) = dom h by MESFUNC2:def 2;
then A20: (max+ h) | E = max+ h by A8, RELAT_1:97;
A21: max+ h is_measurable_on E by A7, MESFUNC2:27, MESFUNC2:37;
for x being set st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:15;
then A22: max- h is nonnegative by SUPINF_2:71;
A23: max K1,1 >= K1 by XXREAL_0:25;
A24: 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 A6;
hence |.((F . n) . x).| <= max K1,1 by A23, XXREAL_0:2; :: thesis:

end;

A25: 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 A26: x in E ; :: thesis:
dom (F . n) = dom |.(F . n).| by MESFUNC1:def 10;
then x in dom |.(F . n).| by A2, A26, MESFUNC8:def 2;
then A27: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def 10;
|.((F . n) . x).| <= max K1,1 by A2, A24, A26;
hence |.(F . n).| . x <= h . x by A9, A26, A27; :: thesis:

end;

for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:14;
then A28: max+ h is nonnegative by SUPINF_2:71;
then A29: dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A22, MESFUNC5:28;
A30: dom (max- h) = dom h by MESFUNC2:def 3;
then A31: (max- h) | E = max- h by A8, RELAT_1:97;
max- h is_measurable_on E by A7, A8, MESFUNC2:28, MESFUNC2:37;
then 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 A8, A19, A30, A21, A28, A22, MESFUNC5:84;
then A32: (integral+ M,(max+ h)) + (integral+ M,(max- h)) < +infty by A8, A19, A30, A29, A20, A31, A18, MESFUNC2:26;
A33: 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 A34: x in dom (lim F) ; :: thesis:
then x in E by A2, MESFUNC8:def 10;
then F # x is convergent by A5;
hence (lim F) . x = (lim_inf F) . x by A34, MESFUNC8:14; :: thesis:

end;

A35: dom (lim_inf F) = dom (F . 0 ) by MESFUNC8:def 8;
A36: h is_measurable_on E by A7, MESFUNC2:37;
then 0 <= integral+ M,(max- h) by A8, A30, A22, MESFUNC2:28, MESFUNC5:85;
then integral+ M,(max+ h) <> +infty by A32, XXREAL_3:def 2;
then A37: integral+ M,(max+ h) < +infty by XXREAL_0:4;
0 <= integral+ M,(max+ h) by A8, A36, A19, A28, MESFUNC2:27, MESFUNC5:85;
then integral+ M,(max- h) <> +infty by A32, XXREAL_3:def 2;
then integral+ M,(max- h) < +infty by XXREAL_0:4;
then A38: h is_integrable_on M by A8, A36, A37, MESFUNC5:def 17;
then A39: 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 A2, A3, A8, A13, A25, Th18;

A40: now

let n be Nat; :: thesis:
A41: E = dom (F . n) by A2, MESFUNC8:def 2;
A42: F . n is_measurable_on E by A3;
|.(F . n).| is_integrable_on M by A2, A3, A8, A38, A25, Th17;
hence F . n is_integrable_on M by A41, A42, MESFUNC5:106; :: thesis:

end;

A43: |.(lim_inf F).| is_integrable_on M by A2, A3, A8, A38, A25, Th17;
dom (lim F) = dom (F . 0 ) by MESFUNC8:def 10;
then A44: lim F = lim_inf F by A35, A33, PARTFUN1:34;
then lim F is_measurable_on E by A2, A3, MESFUNC8:24;
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 A2, A5, A43, A40, A35, A44, A39, MESFUNC5:106; :: thesis: