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 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₁( Nat) -> Element of K16(K17(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 EXTREAL1:23;
- (P . x) <= (F . k) . x by A14, EXTREAL1:23;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A15, MESFUNC5:def 13; :: thesis:

end;

A16: now :: thesis:

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

now :: thesis:

let k be Nat; :: thesis:
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 :: thesis:

let y be ExtReal; :: thesis:
assume y in rng (F # x) ; :: thesis:
then ex k being object 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, EXTREAL1:23; :: thesis:

end;

lim_inf F is E -measurable 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 Element of REAL by A23, XXREAL_0:14;

now :: thesis:

let x be object ; :: 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 :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then G . n = P + (F . n) by A10;
hence G . n is PartFunc of X,ExtREAL ; :: thesis:

end;

A28: now :: thesis:

let n be Nat; :: thesis:
n in 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 Nat; :: 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 :: thesis:

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

end;

deffunc H₂( Nat) -> Element of K16(K17(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 :: thesis:

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 E -measurable by A3;
hence F . n is_integrable_on M by A2, A4, A36, A37, MESFUNC5:102; :: thesis:

end;

A40: now :: thesis:

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

now :: thesis:

let x be object ; :: 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 consider E1 being Element of S such that
AB: ( E1 = dom (G . n) & G . n is E1 -measurable ) ;
for r being Real holds E /\ (less_dom ((G . n),r)) in S

proof

let r be Real; :: thesis:
AC: E1 /\ (less_dom ((G . n),r)) in S by AB;
E = E1 by A30, AB;
hence E /\ (less_dom ((G . n),r)) in S by AC; :: thesis:

end;

hence G . n is E -measurable ; :: 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₃( Nat) -> Element of ExtREAL = Integral (M,(F . $1));
consider I being sequence of 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 in REAL )

proof

let n be Nat; :: thesis:
n in 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 in REAL ) by A50, A52, XXREAL_0:14; :: thesis:

end;

now :: thesis:

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 :: thesis:

let n be Nat; :: thesis:
A59: n in NAT by ORDINAL1:def 12;
H . n = P - (F . n) by A33, A59;
hence H . n is PartFunc of X,ExtREAL ; :: thesis:

end;

A60: now :: thesis:

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

end;

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

A62: now :: thesis:

let x be Element of X; :: thesis:
assume A63: 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:
A64: (superior_realsequence (F # x)) . k >= (F # x) . k by RINFSUP2:8;
(F # x) . k >= - (P . x) by A61, A11, A63;
hence (superior_realsequence (F # x)) . k >= - (P . x) by A64, XXREAL_0:2; :: thesis:

end;

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

now :: thesis:

let y be ExtReal; :: thesis:
assume y in rng (F # x) ; :: thesis:
then ex k being object st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 3;
hence P . x >= y by A61, A11, A63; :: 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 A66: 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 A66, XXREAL_0:2;
then P . x >= (lim_sup F) . x by A63, MESFUNC8:def 8;
hence |.((lim_sup F) . x).| <= P . x by A65, EXTREAL1:23; :: thesis:

end;

lim_sup F is E -measurable by A1, A3, MESFUNC8:23;
then A67: lim_sup F is_integrable_on M by A2, A4, A61, A62, MESFUNC5:102;
then A68: 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, Th13;
set E1 = Integral (M,(lim_sup F));
A69: Integral (M,(lim_sup F)) < +infty by A67, MESFUNC5:96;
-infty < Integral (M,(lim_sup F)) by A67, MESFUNC5:96;
then reconsider e1 = Integral (M,(lim_sup F)) as Element of REAL by A69, XXREAL_0:14;
A70: - (Integral (M,(lim_sup F))) = - e1 by SUPINF_2:2;
A71: P | E = P by A2, RELAT_1:68;
deffunc H₄( Nat) -> Element of K16(K17(X,ExtREAL)) = - (F . $1);
consider F1 being Function such that
A72: ( 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;

A73: now :: thesis:

let n be Nat; :: thesis:
A74: dom (H . n) = dom (P - (F . n)) by A60;
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, A74, MESFUNC1:def 4;
hence dom (H . n) = E ; :: thesis:

end;

now :: thesis:

let n, m be Nat; :: thesis:
thus dom (H . n) = E by A73
.= dom (H . m) by A73 ; :: thesis:

end;

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

A76: now :: thesis:

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

now :: thesis:

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 A77, MESFUNC7:1; :: thesis:
F . n is_integrable_on M by A35;
then H . n is_integrable_on M by A4, A77, Th12;
then consider E4 being Element of S such that
AA: ( E4 = dom (H . n) & H . n is E4 -measurable ) ;
E4 = E by AA, A73;
hence H . n is E -measurable by AA; :: thesis:

end;

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

now :: thesis:

let n be Nat; :: thesis:
A81: n in NAT by ORDINAL1:def 12;
F1 . n = - (F . n) by A72, A81;
hence F1 . n is PartFunc of X,ExtREAL ; :: thesis:

end;

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

A82: now :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence F1 . n = - (F . n) by A72; :: thesis:

end;

now :: thesis:

let n, m be Nat; :: thesis:
F1 . m = - (F . m) by A82;
then A83: dom (F1 . m) = dom (F . m) by MESFUNC1:def 7;
F1 . n = - (F . n) by A82;
then dom (F1 . n) = dom (F . n) by MESFUNC1:def 7;
hence dom (F1 . n) = dom (F1 . m) by A83, MESFUNC8:def 2; :: thesis:

end;

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

A85: now :: thesis:

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

end;

F1 . 0 = - (F . 0) by A82;
then A86: dom (F1 . 0) = dom (F . 0) by MESFUNC1:def 7;
then dom (F1 . 0) = dom (H . 0) by A1, A73;
then lim_inf H = P + (lim_inf F1) by A29, A26, A85, Th11;
then lim_inf H = P + (- (lim_sup F)) by A82, A86, Th15;
then A87: 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 A88: (- (lim_sup F)) | E = - (lim_sup F) by RELAT_1:68;
deffunc H₅( Nat) -> Element of ExtREAL = - (I . $1);
consider I1 being sequence of ExtREAL such that
A89: for n being Element of NAT holds I1 . n = H₅(n) from FUNCT_2:sch 4();
reconsider I1 = I1 as ExtREAL_sequence ;

A90: now :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence I1 . n = - (I . n) by A89; :: thesis:

end;

then A91: - (lim_inf I1) = lim_sup I by Th14;

now :: thesis:

let n be Nat; :: thesis:
A92: F . n is_integrable_on M by A35;
Integral (M,(- (F . n))) = Integral (M,((- 1) (#) (F . n))) by MESFUNC2:9;
then A93: Integral (M,(- (F . n))) = (- jj) * (Integral (M,(F . n))) by A92, MESFUNC5:110;
A94: dom (F . n) = E by A1, MESFUNC8:def 2;
then E = dom (- (F . n)) by MESFUNC1:def 7;
then A95: (- (F . n)) | E = - (F . n) by RELAT_1:68;
H . n = P - (F . n) by A60;
then A96: 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, A92, Th13;
reconsider In = I . n as Element of REAL by A49;
A97: (- 1) * (I . n) = (- 1) * In by EXTREAL1:1;
A98: - (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, A96, A94, A95, A93, A97, A98;
then IH . n = (Integral (M,P)) + (- (I . n)) by A78;
hence IH . n = (Integral (M,P)) + (I1 . n) by A90; :: thesis:

end;

then lim_inf IH = (Integral (M,P)) + (lim_inf I1) by A24, Th10;
then (Integral (M,P)) + ((- jj) * (Integral (M,(lim_sup F)))) <= (Integral (M,P)) + (- (lim_sup I)) by A2, A61, A79, A91, A87, A67, A68, A71, A88, A84, MESFUNC5:110;
then (- 1) * (Integral (M,(lim_sup F))) <= ((- (lim_sup I)) + (Integral (M,P))) - (Integral (M,P)) by A75, A80, XXREAL_3:56;
then (- 1) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + ((Integral (M,P)) - (Integral (M,P))) by A75, A80, XXREAL_3:30;
then A99: (- 1) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + 0. by XXREAL_3:7;
(- 1) * (Integral (M,(lim_sup F))) = (- 1) * e1 by EXTREAL1:1;
then - (Integral (M,(lim_sup F))) <= - (lim_sup I) by A99, A70, XXREAL_3:4;
then A100: Integral (M,(lim_sup F)) >= lim_sup I by XXREAL_3:38;

now :: thesis:

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

end;

A106: 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 A107: x in dom (lim F) ; :: thesis:
then F # x is convergent by A1, A103, A102;
hence (lim F) . x = (lim_sup F) . x by A107, MESFUNC8:14; :: thesis:

end;

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