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 ) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative ) and
A3: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; :: thesis:
A4: ex A being Element of S st
( A = dom P & P is_measurable_on A ) by A1, MESFUNC5:def 17;
then A5: P is_measurable_on E by A1;
for x being set st x in eq_dom P,+infty holds
x in E by A1, MESFUNC1:def 16;
then eq_dom P,+infty c= E by TARSKI:def 3;
then eq_dom P,+infty = E /\ (eq_dom P,+infty ) by XBOOLE_1:28;
then reconsider E0 = eq_dom P,+infty as Element of S by A1, A4, MESFUNC1:37;
reconsider E1 = E \ E0 as Element of S ;
P " {+infty } = E0 by MESFUNC5:36;
then A6: M . E0 = 0 by A1, MESFUNC5:111;
A7: E1 c= E by XBOOLE_1:36;
A8: dom (P | E1) = E1 by A1, RELAT_1:91, XBOOLE_1:36;
set P1 = P | E1;
deffunc H₁( Nat) -> Element of K21(K22(X,ExtREAL )) = (F . $1) | E1;
consider F1 being Functional_Sequence of X,ExtREAL such that
B1: for n being Nat holds F1 . n = H₁(n) from SEQFUNC:sch 1();

B2: 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 B1; :: thesis:

end;

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

now

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

end;

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
P is_measurable_on E1 by A5, MESFUNC1:34, XBOOLE_1:36;
then B4: P | E1 is_integrable_on M by A1, MESFUNC5:118;
B5: P | E1 is nonnegative by A1, MESFUNC5:21;

B6: now

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
assume B61: x in E1 ; :: thesis:
F1 . n = (F . n) | E1 by B1;
then B62: ( (F1 . n) . x = (F . n) . x & (P | E1) . x = P . x ) by B61, FUNCT_1:72;
x in E by A7, B61;
then x in dom (F . n) by A1, MESFUNC8:def 2;
then x in dom |.(F . n).| by MESFUNC1:def 10;
then B63: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def 10;
E1 = dom (F1 . n) by B2;
then E1 = dom |.(F1 . n).| by MESFUNC1:def 10;
then |.(F . n).| . x = |.(F1 . n).| . x by B61, B62, B63, MESFUNC1:def 10;
hence |.(F1 . n).| . x <= (P | E1) . x by B61, A7, A3, B62; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
F . n is_measurable_on E by A1;
then B71: F . n is_measurable_on E1 by MESFUNC1:34, XBOOLE_1:36;
dom (F . n) = E by A1, MESFUNC8:def 2;
then E1 = (dom (F . n)) /\ E1 by XBOOLE_1:28, XBOOLE_1:36;
then (F . n) | E1 is_measurable_on E1 by B71, MESFUNC5:48;
hence F1 . n is_measurable_on E1 by B1; :: thesis:

end;

now

assume eq_dom (P | E1),+infty <> {} ; :: thesis:
then consider x being set such that
B81: x in eq_dom (P | E1),+infty by XBOOLE_0:def 1;
reconsider x = x as Element of X by B81;
( x in dom (P | E1) & (P | E1) . x = +infty ) by B81, MESFUNC1:def 16;
then consider y being R_eal such that
B82: ( y = (P | E1) . x & +infty = y ) ;
B83: x in E1 by A8, B81, MESFUNC1:def 16;
then ( x in dom P & y = P . x & +infty = y ) by A7, A1, B82, FUNCT_1:72;
then x in eq_dom P,+infty by MESFUNC1:def 16;
hence contradiction by B83, XBOOLE_0:def 5; :: thesis:

end;

then consider I being ExtREAL_sequence such that
B9: ( ( for n being Nat holds I . n = Integral M,(F1 . n) ) & lim_inf I >= Integral M,(lim_inf F1) & lim_sup I <= Integral M,(lim_sup F1) & ( ( 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 B3, A8, B4, B5, B6, B7, Th136;
C1: for n being Nat holds I . n = Integral M,(F . n)

proof

let n be Nat; :: thesis:
C11: ( E = dom (F . n) & F . n is_measurable_on E ) by A1, MESFUNC8:def 2;
I . n = Integral M,(F1 . n) by B9;
then C12: I . n = Integral M,((F . n) | E1) by B1;
|.(F . n).| is_integrable_on M by A1, A3, Th136z;
then ( F . n is_integrable_on M & E1 = (dom (F . n)) \ E0 ) by C11, MESFUNC5:106;
then Integral M,(F . n) = (Integral M,((F . n) | E0)) + (Integral M,((F . n) | E1)) by MESFUNC5:105;
then Integral M,(F . n) = 0. + (Integral M,((F . n) | E1)) by C11, A6, MESFUNC5:100;
hence I . n = Integral M,(F . n) by C12, XXREAL_3:4; :: thesis:

end;

C2: ( dom (lim_inf F) = E & lim_inf F is_measurable_on E & dom (lim_sup F) = E & lim_sup F is_measurable_on E ) by A1, MESFUNC8:23, MESFUNC8:24, MESFUNC8:def 8, MESFUNC8:def 9;
then C3: ( Integral M,((lim_inf F) | (E \ E0)) = Integral M,(lim_inf F) & Integral M,((lim_sup F) | (E \ E0)) = Integral M,(lim_sup F) ) by A6, MESFUNC5:101;
( E1 = dom ((lim_inf F) | (E \ E0)) & E1 = dom ((lim_sup F) | (E \ E0)) ) by C2, RELAT_1:91, XBOOLE_1:36;
then C4: ( dom ((lim_inf F) | (E \ E0)) = dom (lim_inf F1) & dom ((lim_sup F) | (E \ E0)) = dom (lim_sup F1) ) by B3, MESFUNC8:def 8, MESFUNC8:def 9;

now

let x be Element of X; :: thesis:
assume C51: x in dom (lim_inf F1) ; :: thesis:
then C52: x in E1 by B3, MESFUNC8:def 8;

now

let n be Element of NAT ; :: thesis:
((F . n) | E1) . x = (F . n) . x by C52, FUNCT_1:72;
then (F1 . n) . x = (F . n) . x by B1;
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 C53: F1 # x = F # x by FUNCT_2:113;
E1 = dom (lim_inf F1) by B3, MESFUNC8:def 8;
then lim_inf (F # x) = (lim_inf F) . x by C51, A7, C2, MESFUNC8:def 8;
then (lim_inf F1) . x = (lim_inf F) . x by C53, C51, MESFUNC8:def 8;
hence ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x by C52, FUNCT_1:72; :: thesis:

end;

then C5: (lim_inf F) | (E \ E0) = lim_inf F1 by C4, PARTFUN1:34;

now

let x be Element of X; :: thesis:
assume C61: x in dom (lim_sup F1) ; :: thesis:
then C62: x in E1 by B3, MESFUNC8:def 9;

now

let n be Element of NAT ; :: thesis:
((F . n) | E1) . x = (F . n) . x by C62, FUNCT_1:72;
then (F1 . n) . x = (F . n) . x by B1;
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 C63: F1 # x = F # x by FUNCT_2:113;
E1 = dom (lim_sup F1) by B3, MESFUNC8:def 9;
then lim_sup (F # x) = (lim_sup F) . x by C61, A7, C2, MESFUNC8:def 9;
then (lim_sup F1) . x = (lim_sup F) . x by C63, C61, MESFUNC8:def 9;
hence ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x by C62, FUNCT_1:72; :: thesis:

end;

then C6: (lim_sup F) | (E \ E0) = lim_sup F1 by C4, PARTFUN1:34;
L2: dom (lim F) = dom (F . 0 ) by MESFUNC8:def 10;
then L3: ( dom (lim F) = dom (lim_sup F) & dom (lim F) = dom (lim_inf F) ) by MESFUNC8:def 8, MESFUNC8:def 9;

now

assume L1: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
L4: 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 L31: x in dom (lim F) ; :: thesis:
then ( x in dom (F . 0 ) & F # x is convergent ) by L1, L2, A1;
hence (lim F) . x = (lim_sup F) . x by L31, MESFUNC8:14; :: thesis:

end;

then L5: lim F = lim_sup F by L3, PARTFUN1:34;
L6: 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 L51: x in dom (lim F) ; :: thesis:
then ( x in dom (F . 0 ) & F # x is convergent ) by L1, L2, A1;
hence (lim F) . x = (lim_inf F) . x by L51, MESFUNC8:14; :: thesis:

end;

then lim F = lim_inf F by L3, PARTFUN1:34;
then L7: lim_sup I <= lim_inf I by L5, C6, B9, C5, XXREAL_0:2;
lim_inf I <= lim_sup I by RINFSUP2:39;
then lim_inf I = lim_sup I by L7, XXREAL_0:1;
hence I is convergent by RINFSUP2:40; :: thesis:
then ( lim I = lim_inf I & lim I = lim_sup I ) by RINFSUP2:41;
then ( Integral M,(lim F) <= lim I & lim I <= Integral M,(lim F) ) by L4, L6, C5, C3, C6, B9, L3, PARTFUN1:34;
hence lim I = Integral M,(lim F) by 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 C1, C5, C3, C6, B9; :: thesis: