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 8;
then A9: (lim_inf F) | E = lim_inf F by RELAT_1:97;
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:60;
- (P . x) <= (F . k) . x by A14, EXTREAL2:60;
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 13;
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 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 5;
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:48;
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 8;
hence |.((lim_inf F) . x).| <= P . x by A19, EXTREAL2:60; :: 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:108;
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:115;
A22: P | E = P by A2, RELAT_1:97;
A23: Integral M,P < +infty by A4, MESFUNC5:102;
-infty < Integral M,P by A4, MESFUNC5:102;
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 13;
0 <= P . x by A5, SUPINF_2:70;
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 13;
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:36;
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:108; :: 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:38;
hence 0 <= (P + (F . n)) . x by A42, MESFUNC1:def 3; :: thesis:

end;

hence G . n is nonnegative by A41, SUPINF_2:71; :: thesis:
F . n is_integrable_on M by A35;
then G . n is_integrable_on M by A4, A41, MESFUNC5:114;
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:102;
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:102;
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 13;
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:102;
-infty < Integral M,(F . n) by A51, MESFUNC5:102;
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:115;
A55: P | E = P by A2, RELAT_1:97;
A56: dom (F . n) = E by A1, MESFUNC8:def 2;
then (F . n) | E = F . n by RELAT_1:97;
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:67;
then Integral M,(lim_inf F) <= (lim_inf I) + ((Integral M,P) - (Integral M,P)) by A48, A46, XXREAL_3:31;
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 13;
hence H . n = P - (F . n) by A33; :: thesis:

end;

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

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

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 5;
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:48;
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 9;
hence |.((lim_sup F) . x).| <= P . x by A64, EXTREAL2:60; :: 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:108;
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:102;
-infty < Integral M,(lim_sup F) by A66, MESFUNC5:102;
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:3;
A70: P | E = P by A2, RELAT_1:97;
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:102;

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:102;

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 13;
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:11;

A83: now

let n be Nat; :: thesis:
H . n = P - (F . n) by A59;
then H . n = P + (- (F . n)) by MESFUNC2:9;
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:9;
E = dom (lim_sup F) by A1, MESFUNC8:def 9;
then E = dom (- (lim_sup F)) by MESFUNC1:def 7;
then A86: (- (lim_sup F)) | E = - (lim_sup F) by RELAT_1:97;
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 13;
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:11;
then A91: Integral M,(- (F . n)) = (R_EAL (- 1)) * (Integral M,(F . n)) by A90, MESFUNC5:116;
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:97;
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:13;
A96: - (I . n) = - In by SUPINF_2:3;
P | E = P by A2, RELAT_1:97;
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:116;
then (R_EAL (- 1)) * (Integral M,(lim_sup F)) <= ((- (lim_sup I)) + (Integral M,P)) - (Integral M,P) by A74, A79, XXREAL_3:67;
then (R_EAL (- 1)) * (Integral M,(lim_sup F)) <= (- (lim_sup I)) + ((Integral M,P) - (Integral M,P)) by A74, A79, XXREAL_3:31;
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:13;
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:40;

now

A99: lim_inf I <= lim_sup I by RINFSUP2:39;
A100: dom (lim F) = dom (F . 0 ) by MESFUNC8:def 10;
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 9;
then A107: lim F = lim_sup F by A104, PARTFUN1:34;
A108: dom (lim F) = dom (lim_inf F) by A100, MESFUNC8:def 8;
then Integral M,(lim F) <= lim_inf I by A57, A102, PARTFUN1:34;
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:34;
lim I = lim_inf I by A109, RINFSUP2:41;
then Integral M,(lim F) <= lim I by A57, A108, A102, PARTFUN1:34;
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: