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 and
A7: eq_dom (P,+infty) = {} ; :: thesis:
A8: E = dom (lim_inf F) by A1, MESFUNC8:def 7;
then A9: (lim_inf F) | E = lim_inf F by RELAT_1:68;
deffunc H₁( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = P + (F . $1);
consider G being Function such that
A10: ( dom G = NAT & ( for n being Element of NAT holds G . n = H₁(n) ) ) from FUNCT_1:sch 4();
A11: for x being Element of X
for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )

proof

let x be Element of X; :: thesis:
let k be Nat; :: thesis:
assume A12: x in E ; :: thesis:
then x in dom (F . k) by A1, MESFUNC8:def 2;
then A13: x in dom |.(F . k).| by MESFUNC1:def 10;
|.(F . k).| . x <= P . x by A6, A12;
then A14: |.((F . k) . x).| <= P . x by A13, MESFUNC1:def 10;
then A15: (F . k) . x <= P . x by EXTREAL2:12;
- (P . x) <= (F . k) . x by A14, EXTREAL2:12;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A15, MESFUNC5:def 13; :: thesis:

end;

A16: now

let x be Element of X; :: thesis:
assume A17: x in dom (lim_inf F) ; :: thesis:

now

let k be Nat; :: thesis:
k is Element of NAT by ORDINAL1:def 12;
then A18: (inferior_realsequence (F # x)) . k <= (F # x) . k by RINFSUP2:8;
(F # x) . k <= P . x by A8, A11, A17;
hence (inferior_realsequence (F # x)) . k <= P . x by A18, XXREAL_0:2; :: thesis:

end;

then lim_inf (F # x) <= P . x by Th5;
then A19: (lim_inf F) . x <= P . x by A17, MESFUNC8:def 7;

now

let y be ext-real number ; :: thesis:
assume y in rng (F # x) ; :: thesis:
then ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 3;
hence - (P . x) <= y by A8, A11, A17; :: thesis:

end;

then - (P . x) is LowerBound of rng (F # x) by XXREAL_2:def 2;
then - (P . x) <= inf (rng (F # x)) by XXREAL_2:def 4;
then - (P . x) <= inf ((F # x) ^\ 0) by NAT_1:47;
then A20: - (P . x) <= (inferior_realsequence (F # x)) . 0 by RINFSUP2:27;
(inferior_realsequence (F # x)) . 0 <= sup (inferior_realsequence (F # x)) by RINFSUP2:23;
then - (P . x) <= lim_inf (F # x) by A20, XXREAL_0:2;
then - (P . x) <= (lim_inf F) . x by A17, MESFUNC8:def 7;
hence |.((lim_inf F) . x).| <= P . x by A19, EXTREAL2:12; :: thesis:

end;

lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24;
then lim_inf F is_integrable_on M by A2, A4, A8, A16, MESFUNC5:102;
then A21: ex E3 being Element of S st
( E3 = (dom P) /\ (dom (lim_inf F)) & Integral (M,(P + (lim_inf F))) = (Integral (M,(P | E3))) + (Integral (M,((lim_inf F) | E3))) ) by A4, MESFUNC5:109;
A22: P | E = P by A2, RELAT_1:68;
A23: Integral (M,P) < +infty by A4, MESFUNC5:96;
-infty < Integral (M,P) by A4, MESFUNC5:96;
then A24: Integral (M,P) is Real by A23, XXREAL_0:14;

now

let x be set ; :: thesis:
assume x in P " {-infty} ; :: thesis:
then A25: P . x in {-infty} by FUNCT_1:def 7;
0 <= P . x by A5, SUPINF_2:51;
hence contradiction by A25, TARSKI:def 1; :: thesis:

end;

then A26: P " {-infty} = {} by XBOOLE_0:def 1;

A27: now

let n be Element of NAT ; :: thesis:
G . n = P + (F . n) by A10;
hence G . n is PartFunc of X,ExtREAL ; :: thesis:

end;

A28: now

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence G . n = P + (F . n) by A10; :: thesis:

end;

reconsider G = G as Functional_Sequence of X,ExtREAL by A10, A27, SEQFUNC:1;
A29: P " {+infty} = {} by A7, MESFUNC5:30;
A30: for n being Nat holds dom (G . n) = E

proof

let n be natural number ; :: thesis:
dom (G . n) = dom (P + (F . n)) by A28;
then A31: dom (G . n) = ((dom P) /\ (dom (F . n))) \ (((P " {-infty}) /\ ((F . n) " {+infty})) \/ ((P " {+infty}) /\ ((F . n) " {-infty}))) by MESFUNC1:def 3;
dom (F . n) = E by A1, MESFUNC8:def 2;
hence dom (G . n) = E by A2, A29, A26, A31; :: thesis:

end;

A32: now

let n, m be natural number ; :: thesis:
thus dom (G . n) = E by A30
.= dom (G . m) by A30 ; :: thesis:

end;

deffunc H₂( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = P - (F . $1);
consider H being Function such that
A33: ( dom H = NAT & ( for n being Element of NAT holds H . n = H₂(n) ) ) from FUNCT_1:sch 4();
reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A32, MESFUNC8:def 2;
A34: dom (G . 0) = dom (F . 0) by A1, A30;
A35: for n being Nat holds F . n is_integrable_on M

proof

let n be Nat; :: thesis:
A36: E = dom (F . n) by A1, MESFUNC8:def 2;

A37: now

let x be Element of X; :: thesis:
assume A38: x in dom (F . n) ; :: thesis:
then A39: x in dom |.(F . n).| by MESFUNC1:def 10;
|.(F . n).| . x <= P . x by A6, A36, A38;
hence |.((F . n) . x).| <= P . x by A39, MESFUNC1:def 10; :: thesis:

end;

F . n is_measurable_on E by A3;
hence F . n is_integrable_on M by A2, A4, A36, A37, MESFUNC5:102; :: thesis:

end;

A40: now

let n be Nat; :: thesis:
A41: G . n = P + (F . n) by A28;

now

let x be set ; :: thesis:
assume A42: x in dom (P + (F . n)) ; :: thesis:
then reconsider x1 = x as Element of X ;
x in E by A30, A41, A42;
then - (P . x) <= (F # x1) . n by A11;
then A43: - (P . x) <= (F . n) . x by MESFUNC5:def 13;
(- (P . x)) + (P . x) = 0 by XXREAL_3:7;
then 0 <= ((F . n) . x) + (P . x) by A43, XXREAL_3:36;
hence 0 <= (P + (F . n)) . x by A42, MESFUNC1:def 3; :: thesis:

end;

hence G . n is nonnegative by A41, SUPINF_2:52; :: thesis:
F . n is_integrable_on M by A35;
then G . n is_integrable_on M by A4, A41, MESFUNC5:108;
then ex E1 being Element of S st
( E1 = dom (G . n) & G . n is_measurable_on E1 ) by MESFUNC5:def 17;
hence G . n is_measurable_on E by A30; :: thesis:

end;

E = dom (G . 0) by A30;
then consider IG being ExtREAL_sequence such that
A44: for n being Nat holds IG . n = Integral (M,(G . n)) and
A45: Integral (M,(lim_inf G)) <= lim_inf IG by A40, Th7;
A46: Integral (M,P) < +infty by A4, MESFUNC5:96;
deffunc H₃( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . $1));
consider I being Function of NAT,ExtREAL such that
A47: for n being Element of NAT holds I . n = H₃(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
A48: -infty < Integral (M,P) by A4, MESFUNC5:96;
A49: for n being Nat holds
( I . n = Integral (M,(F . n)) & I . n is Real )

proof

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
then A50: I . n = Integral (M,(F . n)) by A47;
A51: F . n is_integrable_on M by A35;
then A52: Integral (M,(F . n)) < +infty by MESFUNC5:96;
-infty < Integral (M,(F . n)) by A51, MESFUNC5:96;
hence ( I . n = Integral (M,(F . n)) & I . n is Real ) by A50, A52, XXREAL_0:14; :: thesis:

end;

now

let n be Nat; :: thesis:
A53: G . n = P + (F . n) by A28;
F . n is_integrable_on M by A35;
then A54: ex E2 being Element of S st
( E2 = (dom P) /\ (dom (F . n)) & Integral (M,(G . n)) = (Integral (M,(P | E2))) + (Integral (M,((F . n) | E2))) ) by A4, A53, MESFUNC5:109;
A55: P | E = P by A2, RELAT_1:68;
A56: dom (F . n) = E by A1, MESFUNC8:def 2;
then (F . n) | E = F . n by RELAT_1:68;
then Integral (M,(G . n)) = (Integral (M,P)) + (I . n) by A2, A49, A54, A56, A55;
hence IG . n = (Integral (M,P)) + (I . n) by A44; :: thesis:

end;

then lim_inf IG = (Integral (M,P)) + (lim_inf I) by A24, Th10;
then (Integral (M,P)) + (Integral (M,(lim_inf F))) <= (Integral (M,P)) + (lim_inf I) by A2, A8, A28, A29, A26, A45, A21, A22, A9, A34, Th11;
then Integral (M,(lim_inf F)) <= ((lim_inf I) + (Integral (M,P))) - (Integral (M,P)) by A48, A46, XXREAL_3:56;
then Integral (M,(lim_inf F)) <= (lim_inf I) + ((Integral (M,P)) - (Integral (M,P))) by A48, A46, XXREAL_3:30;
then Integral (M,(lim_inf F)) <= (lim_inf I) + 0. by XXREAL_3:7;
then A57: Integral (M,(lim_inf F)) <= lim_inf I by XXREAL_3:4;

A58: now

let n be Element of NAT ; :: thesis:
H . n = P - (F . n) by A33;
hence H . n is PartFunc of X,ExtREAL ; :: thesis:

end;

A59: now

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence H . n = P - (F . n) by A33; :: thesis:

end;

A60: E = dom (lim_sup F) by A1, MESFUNC8:def 8;

A61: now

let x be Element of X; :: thesis:
assume A62: x in dom (lim_sup F) ; :: thesis:
for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)

proof

let k be Nat; :: thesis:
k is Element of NAT by ORDINAL1:def 12;
then A63: (superior_realsequence (F # x)) . k >= (F # x) . k by RINFSUP2:8;
(F # x) . k >= - (P . x) by A60, A11, A62;
hence (superior_realsequence (F # x)) . k >= - (P . x) by A63, XXREAL_0:2; :: thesis:

end;

then lim_sup (F # x) >= - (P . x) by Th4;
then A64: (lim_sup F) . x >= - (P . x) by A62, MESFUNC8:def 8;

now

let y be ext-real number ; :: thesis:
assume y in rng (F # x) ; :: thesis:
then ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 3;
hence P . x >= y by A60, A11, A62; :: thesis:

end;

then P . x is UpperBound of rng (F # x) by XXREAL_2:def 1;
then P . x >= sup (rng (F # x)) by XXREAL_2:def 3;
then P . x >= sup ((F # x) ^\ 0) by NAT_1:47;
then A65: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27;
(superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23;
then P . x >= lim_sup (F # x) by A65, XXREAL_0:2;
then P . x >= (lim_sup F) . x by A62, MESFUNC8:def 8;
hence |.((lim_sup F) . x).| <= P . x by A64, EXTREAL2:12; :: thesis:

end;

lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23;
then A66: lim_sup F is_integrable_on M by A2, A4, A60, A61, MESFUNC5:102;
then A67: ex E6 being Element of S st
( E6 = (dom P) /\ (dom (lim_sup F)) & Integral (M,(P - (lim_sup F))) = (Integral (M,(P | E6))) + (Integral (M,((- (lim_sup F)) | E6))) ) by A4, Th14;
set E1 = Integral (M,(lim_sup F));
A68: Integral (M,(lim_sup F)) < +infty by A66, MESFUNC5:96;
-infty < Integral (M,(lim_sup F)) by A66, MESFUNC5:96;
then reconsider e1 = Integral (M,(lim_sup F)) as Real by A68, XXREAL_0:14;
A69: - (Integral (M,(lim_sup F))) = - e1 by SUPINF_2:2;
A70: P | E = P by A2, RELAT_1:68;
deffunc H₄( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = - (F . $1);
consider F1 being Function such that
A71: ( dom F1 = NAT & ( for n being Element of NAT holds F1 . n = H₄(n) ) ) from FUNCT_1:sch 4();
reconsider H = H as Functional_Sequence of X,ExtREAL by A33, A58, SEQFUNC:1;

A72: now

let n be natural number ; :: thesis:
A73: dom (H . n) = dom (P - (F . n)) by A59;
dom (F . n) = E by A1, MESFUNC8:def 2;
then dom (H . n) = (E /\ E) \ (({} /\ ((F . n) " {+infty})) \/ ({} /\ ((F . n) " {-infty}))) by A2, A29, A26, A73, MESFUNC1:def 4;
hence dom (H . n) = E ; :: thesis:

end;

now

let n, m be natural number ; :: thesis:
thus dom (H . n) = E by A72
.= dom (H . m) by A72 ; :: thesis:

end;

then reconsider H = H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
A74: -infty < Integral (M,P) by A4, MESFUNC5:96;

A75: now

let n be Nat; :: thesis:
A76: H . n = P - (F . n) by A59;

now

let x be Element of X; :: thesis:
assume x in dom (F . n) ; :: thesis:
then x in E by A1, MESFUNC8:def 2;
then (F # x) . n <= P . x by A11;
hence (F . n) . x <= P . x by MESFUNC5:def 13; :: thesis:

end;

hence H . n is nonnegative by A76, MESFUNC7:1; :: thesis:
F . n is_integrable_on M by A35;
then H . n is_integrable_on M by A4, A76, Th13;
then ex E4 being Element of S st
( E4 = dom (H . n) & H . n is_measurable_on E4 ) by MESFUNC5:def 17;
hence H . n is_measurable_on E by A72; :: thesis:

end;

E = dom (H . 0) by A72;
then consider IH being ExtREAL_sequence such that
A77: for n being Nat holds IH . n = Integral (M,(H . n)) and
A78: Integral (M,(lim_inf H)) <= lim_inf IH by A75, Th7;
A79: Integral (M,P) < +infty by A4, MESFUNC5:96;

now

let n be Element of NAT ; :: thesis:
F1 . n = - (F . n) by A71;
hence F1 . n is PartFunc of X,ExtREAL ; :: thesis:

end;

then reconsider F1 = F1 as Functional_Sequence of X,ExtREAL by A71, SEQFUNC:1;

A80: now

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence F1 . n = - (F . n) by A71; :: thesis:

end;

now

let n, m be natural number ; :: thesis:
F1 . m = - (F . m) by A80;
then A81: dom (F1 . m) = dom (F . m) by MESFUNC1:def 7;
F1 . n = - (F . n) by A80;
then dom (F1 . n) = dom (F . n) by MESFUNC1:def 7;
hence dom (F1 . n) = dom (F1 . m) by A81, MESFUNC8:def 2; :: thesis:

end;

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
A82: Integral (M,(- (lim_sup F))) = Integral (M,((- 1) (#) (lim_sup F))) by MESFUNC2:9;

A83: now

let n be Nat; :: thesis:
H . n = P - (F . n) by A59;
then H . n = P + (- (F . n)) by MESFUNC2:8;
hence H . n = P + (F1 . n) by A80; :: thesis:

end;

F1 . 0 = - (F . 0) by A80;
then A84: dom (F1 . 0) = dom (F . 0) by MESFUNC1:def 7;
then dom (F1 . 0) = dom (H . 0) by A1, A72;
then lim_inf H = P + (lim_inf F1) by A29, A26, A83, Th11;
then lim_inf H = P + (- (lim_sup F)) by A80, A84, Th16;
then A85: lim_inf H = P - (lim_sup F) by MESFUNC2:8;
E = dom (lim_sup F) by A1, MESFUNC8:def 8;
then E = dom (- (lim_sup F)) by MESFUNC1:def 7;
then A86: (- (lim_sup F)) | E = - (lim_sup F) by RELAT_1:68;
deffunc H₅( Element of NAT ) -> Element of ExtREAL = - (I . $1);
consider I1 being Function of NAT,ExtREAL such that
A87: for n being Element of NAT holds I1 . n = H₅(n) from FUNCT_2:sch 4();
reconsider I1 = I1 as ExtREAL_sequence ;

A88: now

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence I1 . n = - (I . n) by A87; :: thesis:

end;

then A89: - (lim_inf I1) = lim_sup I by Th15;

now

let n be Nat; :: thesis:
A90: F . n is_integrable_on M by A35;
Integral (M,(- (F . n))) = Integral (M,((- 1) (#) (F . n))) by MESFUNC2:9;
then A91: Integral (M,(- (F . n))) = (R_EAL (- 1)) * (Integral (M,(F . n))) by A90, MESFUNC5:110;
A92: dom (F . n) = E by A1, MESFUNC8:def 2;
then E = dom (- (F . n)) by MESFUNC1:def 7;
then A93: (- (F . n)) | E = - (F . n) by RELAT_1:68;
H . n = P - (F . n) by A59;
then A94: ex E5 being Element of S st
( E5 = (dom P) /\ (dom (F . n)) & Integral (M,(H . n)) = (Integral (M,(P | E5))) + (Integral (M,((- (F . n)) | E5))) ) by A4, A90, Th14;
reconsider In = I . n as Real by A49;
A95: (R_EAL (- 1)) * (I . n) = (- 1) * In by EXTREAL1:1;
A96: - (I . n) = - In by SUPINF_2:2;
P | E = P by A2, RELAT_1:68;
then Integral (M,(H . n)) = (Integral (M,P)) + (- (I . n)) by A2, A49, A94, A92, A93, A91, A95, A96;
then IH . n = (Integral (M,P)) + (- (I . n)) by A77;
hence IH . n = (Integral (M,P)) + (I1 . n) by A88; :: thesis:

end;

then lim_inf IH = (Integral (M,P)) + (lim_inf I1) by A24, Th10;
then (Integral (M,P)) + ((R_EAL (- 1)) * (Integral (M,(lim_sup F)))) <= (Integral (M,P)) + (- (lim_sup I)) by A2, A60, A78, A89, A85, A66, A67, A70, A86, A82, MESFUNC5:110;
then (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= ((- (lim_sup I)) + (Integral (M,P))) - (Integral (M,P)) by A74, A79, XXREAL_3:56;
then (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + ((Integral (M,P)) - (Integral (M,P))) by A74, A79, XXREAL_3:30;
then A97: (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + 0. by XXREAL_3:7;
(R_EAL (- 1)) * (Integral (M,(lim_sup F))) = (- 1) * e1 by EXTREAL1:1;
then - (Integral (M,(lim_sup F))) <= - (lim_sup I) by A97, A69, XXREAL_3:4;
then A98: Integral (M,(lim_sup F)) >= lim_sup I by XXREAL_3:38;

now

A99: lim_inf I <= lim_sup I by RINFSUP2:39;
A100: dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
assume A101: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
A102: 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 A103: x in dom (lim F) ; :: thesis:
then F # x is convergent by A1, A101, A100;
hence (lim F) . x = (lim_inf F) . x by A103, MESFUNC8:14; :: thesis:

end;

A104: 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 A105: x in dom (lim F) ; :: thesis:
then F # x is convergent by A1, A101, A100;
hence (lim F) . x = (lim_sup F) . x by A105, MESFUNC8:14; :: thesis:

end;

A106: dom (lim F) = dom (lim_sup F) by A100, MESFUNC8:def 8;
then A107: lim F = lim_sup F by A104, PARTFUN1:5;
A108: dom (lim F) = dom (lim_inf F) by A100, MESFUNC8:def 7;
then Integral (M,(lim F)) <= lim_inf I by A57, A102, PARTFUN1:5;
then lim_sup I <= lim_inf I by A98, A107, XXREAL_0:2;
then lim_inf I = lim_sup I by A99, XXREAL_0:1;
hence A109: I is convergent by RINFSUP2:40; :: thesis:
then lim I = lim_sup I by RINFSUP2:41;
then A110: lim I <= Integral (M,(lim F)) by A98, A106, A104, PARTFUN1:5;
lim I = lim_inf I by A109, RINFSUP2:41;
then Integral (M,(lim F)) <= lim I by A57, A108, A102, PARTFUN1:5;
hence lim I = Integral (M,(lim F)) by A110, 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 A49, A57, A98; :: thesis: