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:
let P be PartFunc of X,ExtREAL; :: 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: P is nonnegative and
A6: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; :: thesis:
for x being object st x in eq_dom (P,+infty) holds
x in E by A2, MESFUNC1:def 15;
then eq_dom (P,+infty) c= E by TARSKI:def 3;
then A7: eq_dom (P,+infty) = E /\ (eq_dom (P,+infty)) by XBOOLE_1:28;
ex A being Element of S st
( A = dom P & P is A -measurable ) by A4;
then reconsider E0 = eq_dom (P,+infty) as Element of S by A2, A7, MESFUNC1:33;
reconsider E1 = E \ E0 as Element of S ;
deffunc H₁( Nat) -> Element of K16(K17(X,ExtREAL)) = (F . $1) | E1;
consider F1 being Functional_Sequence of X,ExtREAL such that
A8: for n being Nat holds F1 . n = H₁(n) from SEQFUNC:sch 1();

A9: now :: thesis:

let n be Nat; :: thesis:
dom (F . n) = E by A1, MESFUNC8:def 2;
then dom ((F . n) | E1) = E1 by RELAT_1:62, XBOOLE_1:36;
hence dom (F1 . n) = E1 by A8; :: thesis:

end;

then A10: E1 = dom (F1 . 0) ;

now :: thesis:

let n, m be Nat; :: thesis:
thus dom (F1 . n) = E1 by A9
.= dom (F1 . m) by A9 ; :: thesis:

end;

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
set P1 = P | E1;
A11: P | E1 is nonnegative by A5, MESFUNC5:15;
A12: E1 c= E by XBOOLE_1:36;

A13: now :: thesis:

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
assume A14: x in E1 ; :: thesis:
then A15: (P | E1) . x = P . x by FUNCT_1:49;
x in E by A12, A14;
then x in dom (F . n) by A1, MESFUNC8:def 2;
then x in dom |.(F . n).| by MESFUNC1:def 10;
then A16: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def 10;
E1 = dom (F1 . n) by A9;
then A17: E1 = dom |.(F1 . n).| by MESFUNC1:def 10;
F1 . n = (F . n) | E1 by A8;
then (F1 . n) . x = (F . n) . x by A14, FUNCT_1:49;
then |.(F . n).| . x = |.(F1 . n).| . x by A14, A16, A17, MESFUNC1:def 10;
hence |.(F1 . n).| . x <= (P | E1) . x by A6, A12, A14, A15; :: thesis:

end;

A18: dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
then A19: dom (lim F) = dom (lim_inf F) by MESFUNC8:def 7;
A20: dom (lim_inf F) = E by A1, MESFUNC8:def 7;

A21: now :: thesis:

let x be Element of X; :: thesis:
assume A22: x in dom (lim_inf F1) ; :: thesis:
then A23: x in E1 by A10, MESFUNC8:def 7;

now :: thesis:

let n be Element of NAT ; :: thesis:
((F . n) | E1) . x = (F . n) . x by A23, FUNCT_1:49;
then (F1 . n) . x = (F . n) . x by A8;
then (F1 # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F1 # x) . n = (F # x) . n by MESFUNC5:def 13; :: thesis:

end;

then A24: F1 # x = F # x by FUNCT_2:63;
E1 = dom (lim_inf F1) by A10, MESFUNC8:def 7;
then lim_inf (F # x) = (lim_inf F) . x by A12, A20, A22, MESFUNC8:def 7;
then (lim_inf F1) . x = (lim_inf F) . x by A22, A24, MESFUNC8:def 7;
hence ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x by A23, FUNCT_1:49; :: thesis:

end;

E1 = dom ((lim_inf F) | (E \ E0)) by A20, RELAT_1:62, XBOOLE_1:36;
then dom ((lim_inf F) | (E \ E0)) = dom (lim_inf F1) by A10, MESFUNC8:def 7;
then A25: (lim_inf F) | (E \ E0) = lim_inf F1 by A21, PARTFUN1:5;
A26: dom (lim_sup F) = E by A1, MESFUNC8:def 8;

A27: now :: thesis:

let x be Element of X; :: thesis:
assume A28: x in dom (lim_sup F1) ; :: thesis:
then A29: x in E1 by A10, MESFUNC8:def 8;

now :: thesis:

let n be Element of NAT ; :: thesis:
((F . n) | E1) . x = (F . n) . x by A29, FUNCT_1:49;
then (F1 . n) . x = (F . n) . x by A8;
then (F1 # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F1 # x) . n = (F # x) . n by MESFUNC5:def 13; :: thesis:

end;

then A30: F1 # x = F # x by FUNCT_2:63;
E1 = dom (lim_sup F1) by A10, MESFUNC8:def 8;
then lim_sup (F # x) = (lim_sup F) . x by A12, A26, A28, MESFUNC8:def 8;
then (lim_sup F1) . x = (lim_sup F) . x by A28, A30, MESFUNC8:def 8;
hence ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x by A29, FUNCT_1:49; :: thesis:

end;

E1 = dom ((lim_sup F) | (E \ E0)) by A26, RELAT_1:62, XBOOLE_1:36;
then dom ((lim_sup F) | (E \ E0)) = dom (lim_sup F1) by A10, MESFUNC8:def 8;
then A31: (lim_sup F) | (E \ E0) = lim_sup F1 by A27, PARTFUN1:5;
A32: dom (P | E1) = E1 by A2, RELAT_1:62, XBOOLE_1:36;

A33: now :: thesis:

assume eq_dom ((P | E1),+infty) <> {} ; :: thesis:
then consider x being object such that
A34: x in eq_dom ((P | E1),+infty) by XBOOLE_0:def 1;
reconsider x = x as Element of X by A34;
(P | E1) . x = +infty by A34, MESFUNC1:def 15;
then consider y being R_eal such that
A35: y = (P | E1) . x and
A36: +infty = y ;
A37: x in E1 by A32, A34, MESFUNC1:def 15;
then y = P . x by A35, FUNCT_1:49;
then x in eq_dom (P,+infty) by A2, A12, A36, A37, MESFUNC1:def 15;
hence contradiction by A37, XBOOLE_0:def 5; :: thesis:

end;

A38: for n being Nat holds F1 . n is E1 -measurable

proof

let n be Nat; :: thesis:
dom (F . n) = E by A1, MESFUNC8:def 2;
then A39: E1 = (dom (F . n)) /\ E1 by XBOOLE_1:28, XBOOLE_1:36;
F . n is E -measurable by A3;
then F . n is E1 -measurable by MESFUNC1:30, XBOOLE_1:36;
then (F . n) | E1 is E1 -measurable by A39, MESFUNC5:42;
hence F1 . n is E1 -measurable by A8; :: thesis:

end;

P | E1 is_integrable_on M by A4, MESFUNC5:112;
then consider I being ExtREAL_sequence such that
A40: for n being Nat holds I . n = Integral (M,(F1 . n)) and
A41: lim_inf I >= Integral (M,(lim_inf F1)) and
A42: lim_sup I <= Integral (M,(lim_sup F1)) and
( ( for x being Element of X st x in E1 holds
F1 # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F1)) ) ) by A32, A10, A11, A13, A38, A33, Lm1;
P " {+infty} = E0 by MESFUNC5:30;
then A43: M . E0 = 0 by A4, MESFUNC5:105;
A44: for n being Nat holds I . n = Integral (M,(F . n))

proof

let n be Nat; :: thesis:
A45: E = dom (F . n) by A1, MESFUNC8:def 2;
A46: F . n is E -measurable by A3;
|.(F . n).| is_integrable_on M by A1, A2, A3, A4, A6, Th16;
then F . n is_integrable_on M by A45, A46, MESFUNC5:100;
then Integral (M,(F . n)) = (Integral (M,((F . n) | E0))) + (Integral (M,((F . n) | E1))) by A45, MESFUNC5:99;
then A47: Integral (M,(F . n)) = 0. + (Integral (M,((F . n) | E1))) by A3, A43, A45, MESFUNC5:94;
I . n = Integral (M,(F1 . n)) by A40;
then I . n = Integral (M,((F . n) | E1)) by A8;
hence I . n = Integral (M,(F . n)) by A47, XXREAL_3:4; :: thesis:

end;

lim_inf F is E -measurable by A1, A3, MESFUNC8:24;
then A48: Integral (M,((lim_inf F) | (E \ E0))) = Integral (M,(lim_inf F)) by A43, A20, MESFUNC5:95;
lim_sup F is E -measurable by A1, A3, MESFUNC8:23;
then A49: Integral (M,((lim_sup F) | (E \ E0))) = Integral (M,(lim_sup F)) by A43, A26, MESFUNC5:95;
A50: dom (lim F) = dom (lim_sup F) by A18, MESFUNC8:def 8;

now :: thesis:

assume A51: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
A52: 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 A53: x in dom (lim F) ; :: thesis:
then F # x is convergent by A1, A18, A51;
hence (lim F) . x = (lim_inf F) . x by A53, MESFUNC8:14; :: thesis:

end;

then A54: lim F = lim_inf F by A19, PARTFUN1:5;
A55: lim_inf I <= lim_sup I by RINFSUP2:39;
A56: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_sup F) . x

proof

let x be Element of X; :: thesis:
assume A57: x in dom (lim F) ; :: thesis:
then F # x is convergent by A1, A18, A51;
hence (lim F) . x = (lim_sup F) . x by A57, MESFUNC8:14; :: thesis:

end;

then lim F = lim_sup F by A50, PARTFUN1:5;
then lim_sup I <= lim_inf I by A41, A42, A25, A31, A54, XXREAL_0:2;
then lim_inf I = lim_sup I by A55, XXREAL_0:1;
hence A58: I is convergent by RINFSUP2:40; :: thesis:
then lim I = lim_sup I by RINFSUP2:41;
then A59: lim I <= Integral (M,(lim F)) by A42, A49, A31, A50, A56, PARTFUN1:5;
lim I = lim_inf I by A58, RINFSUP2:41;
then Integral (M,(lim F)) <= lim I by A41, A48, A25, A19, A52, PARTFUN1:5;
hence lim I = Integral (M,(lim F)) by A59, XXREAL_0:1; :: thesis:

end;

hence 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 A41, A42, A44, A48, A49, A25, A31; :: thesis: