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_measurable_on E 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 set st x in eq_dom P,+infty holds
x in E by A2, MESFUNC1:def 16;
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_measurable_on A ) by A4, MESFUNC5:def 17;
then reconsider E0 = eq_dom P,+infty as Element of S by A2, A7, MESFUNC1:37;
reconsider E1 = E \ E0 as Element of S ;
deffunc H₁( Nat) -> Element of K6(K7(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

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

end;

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

now

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:21;
A12: E1 c= E by XBOOLE_1:36;

A13: now

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:72;
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:72;
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 10;
then A19: dom (lim F) = dom (lim_inf F) by MESFUNC8:def 8;
A20: dom (lim_inf F) = E by A1, MESFUNC8:def 8;

A21: now

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 8;

now

let n be Element of NAT ; :: thesis:
((F . n) | E1) . x = (F . n) . x by A23, FUNCT_1:72;
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:113;
E1 = dom (lim_inf F1) by A10, MESFUNC8:def 8;
then lim_inf (F # x) = (lim_inf F) . x by A12, A20, A22, MESFUNC8:def 8;
then (lim_inf F1) . x = (lim_inf F) . x by A22, A24, MESFUNC8:def 8;
hence ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x by A23, FUNCT_1:72; :: thesis:

end;

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

A27: now

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 9;

now

let n be Element of NAT ; :: thesis:
((F . n) | E1) . x = (F . n) . x by A29, FUNCT_1:72;
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:113;
E1 = dom (lim_sup F1) by A10, MESFUNC8:def 9;
then lim_sup (F # x) = (lim_sup F) . x by A12, A26, A28, MESFUNC8:def 9;
then (lim_sup F1) . x = (lim_sup F) . x by A28, A30, MESFUNC8:def 9;
hence ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x by A29, FUNCT_1:72; :: thesis:

end;

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

A33: now

assume eq_dom (P | E1),+infty <> {} ; :: thesis:
then consider x being set 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 16;
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 16;
then y = P . x by A35, FUNCT_1:72;
then x in eq_dom P,+infty by A2, A12, A36, A37, MESFUNC1:def 16;
hence contradiction by A37, XBOOLE_0:def 5; :: thesis:

end;

A38: for n being Nat holds F1 . n is_measurable_on E1

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_measurable_on E by A3;
then F . n is_measurable_on E1 by MESFUNC1:34, XBOOLE_1:36;
then (F . n) | E1 is_measurable_on E1 by A39, MESFUNC5:48;
hence F1 . n is_measurable_on E1 by A8; :: thesis:

end;

P | E1 is_integrable_on M by A4, MESFUNC5:118;
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:36;
then A43: M . E0 = 0 by A4, MESFUNC5:111;
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_measurable_on E by A3;
|.(F . n).| is_integrable_on M by A1, A2, A3, A4, A6, Th17;
then F . n is_integrable_on M by A45, A46, MESFUNC5:106;
then Integral M,(F . n) = (Integral M,((F . n) | E0)) + (Integral M,((F . n) | E1)) by A45, MESFUNC5:105;
then A47: Integral M,(F . n) = 0. + (Integral M,((F . n) | E1)) by A3, A43, A45, MESFUNC5:100;
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_measurable_on E by A1, A3, MESFUNC8:24;
then A48: Integral M,((lim_inf F) | (E \ E0)) = Integral M,(lim_inf F) by A43, A20, MESFUNC5:101;
lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23;
then A49: Integral M,((lim_sup F) | (E \ E0)) = Integral M,(lim_sup F) by A43, A26, MESFUNC5:101;
A50: dom (lim F) = dom (lim_sup F) by A18, MESFUNC8:def 9;

now

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:34;
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:34;
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:34;
lim I = lim_inf I by A58, RINFSUP2:41;
then Integral M,(lim F) <= lim I by A41, A48, A25, A19, A52, PARTFUN1:34;
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: