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 E -measurable 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 such that
A6: for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K1 by A4;
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 object st x in E holds
h . x = max (K1,1) by MESFUNC5:41, NUMBERS:31;
A10: dom h = dom |.h.| by MESFUNC1:def 10;
A11: max (K1,1) > 0 by XXREAL_0:30;
then A12: (max (K1,1)) * +infty = +infty by XXREAL_3:def 5;
for x being object st x in E holds
h . x >= 0. by A11, A9;
then A13: h is nonnegative by A8, SUPINF_2:52;
then A14: Integral (M,h) = integral' (M,h) by A7, MESFUNC5:89;
A15: integral' (M,h) = (max (K1,1)) * (M . (dom h)) by A11, A8, A9, MESFUNC5:104;
A16: for x being Element of X st x in dom h holds
h . x = |.h.| . x

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:51;
then |.(h . x).| = h . x by EXTREAL1:def 1;
hence h . x = |.h.| . x by A17, MESFUNC1:def 10; :: thesis:

end;

Integral (M,h) = integral+ (M,h) by A7, A13, MESFUNC5:89;
then integral+ (M,h) < +infty by A1, A11, A8, A15, A12, A14, XXREAL_3:72;
then A18: integral+ (M,|.h.|) < +infty by A10, A16, PARTFUN1:5;
A19: dom (max+ h) = dom h by MESFUNC2:def 2;
then A20: (max+ h) | E = max+ h by A8, RELAT_1:68;
A21: max+ h is E -measurable by A7, MESFUNC2:25, MESFUNC2:34;
for x being object st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:13;
then A22: max- h is nonnegative by SUPINF_2:52;
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)

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

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 object st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:12;
then A28: max+ h is nonnegative by SUPINF_2:52;
then A29: dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A22, MESFUNC5:22;
A30: dom (max- h) = dom h by MESFUNC2:def 3;
then A31: (max- h) | E = max- h by A8, RELAT_1:68;
max- h is E -measurable by A7, A8, MESFUNC2:26, MESFUNC2:34;
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:78;
then A32: (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) < +infty by A8, A19, A30, A29, A20, A31, A18, MESFUNC2:24;
A33: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_inf F) . x

let x be Element of X; :: thesis:
assume A34: x in dom (lim F) ; :: thesis:
then x in E by A2, MESFUNC8:def 9;
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 7;
A36: h is E -measurable by A7, MESFUNC2:34;
then 0 <= integral+ (M,(max- h)) by A8, A30, A22, MESFUNC2:26, MESFUNC5:79;
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:25, MESFUNC5:79;
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;
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, Th17;

A40: now :: thesis:

let n be Nat; :: thesis:
A41: E = dom (F . n) by A2, MESFUNC8:def 2;
A42: F . n is E -measurable by A3;
|.(F . n).| is_integrable_on M by A2, A3, A8, A38, A25, Th16;
hence F . n is_integrable_on M by A41, A42, MESFUNC5:100; :: thesis:

end;

A43: |.(lim_inf F).| is_integrable_on M by A2, A3, A8, A38, A25, Th16;
dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
then A44: lim F = lim_inf F by A35, A33, PARTFUN1:5;
then lim F is E -measurable 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:100; :: thesis: