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 ) and
A2: for n being Nat holds F . n is_measurable_on E and
A3: ( P is_integrable_on M & P is nonnegative ) and
A4: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A5: eq_dom P,+infty = {} ; :: thesis:
A6: for n being Nat holds F . n is_integrable_on M

proof

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

now

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

end;

hence F . n is_integrable_on M by A61, A1, A3, MESFUNC5:108; :: thesis:

end;

A7: ( E = dom (lim_inf F) & E = dom (lim_sup F) ) by A1, MESFUNC8:def 8, MESFUNC8:def 9;
A8: ( lim_inf F is_measurable_on E & lim_sup F is_measurable_on E ) by A1, A2, MESFUNC8:23, MESFUNC8:24;
A9: 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 A91: x in E ; :: thesis:
then x in dom (F . k) by A1, MESFUNC8:def 2;
then A92: x in dom |.(F . k).| by MESFUNC1:def 10;
|.(F . k).| . x <= P . x by A4, A91;
then |.((F . k) . x).| <= P . x by A92, MESFUNC1:def 10;
then ( - (P . x) <= (F . k) . x & (F . k) . x <= P . x ) by EXTREAL2:60;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by MESFUNC5:def 13; :: thesis:

end;

deffunc H₁( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
consider I being Function of NAT ,ExtREAL such that
B1: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
B2: 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 B21: I . n = Integral M,(F . n) by B1;
F . n is_integrable_on M by A6;
then ( -infty < Integral M,(F . n) & Integral M,(F . n) < +infty ) by MESFUNC5:102;
hence ( I . n = Integral M,(F . n) & I . n is Real ) by B21, XXREAL_0:14; :: thesis:

end;

deffunc H₂( Element of NAT ) -> Element of K21(K22(X,ExtREAL )) = P + (F . $1);
consider G being Function such that
B3: ( dom G = NAT & ( for n being Element of NAT holds G . n = H₂(n) ) ) from FUNCT_1:sch 4();

B8: now

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

end;

now

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

end;

then reconsider G = G as Functional_Sequence of X,ExtREAL by B3, SEQFUNC:1;
B4: P " {+infty } = {} by A5, MESFUNC5:36;

now

let x be set ; :: thesis:
assume x in P " {-infty } ; :: thesis:
then B51: ( x in dom P & P . x in {-infty } ) by FUNCT_1:def 13;
( -infty < 0 & 0 <= P . x ) by A3, SUPINF_2:70;
hence contradiction by B51, TARSKI:def 1; :: thesis:

end;

then B5: P " {-infty } = {} by XBOOLE_0:def 1;
B6: for n being Nat holds dom (G . n) = E

proof

let n be natural number ; :: thesis:
B61: dom (F . n) = E by A1, MESFUNC8:def 2;
dom (G . n) = dom (P + (F . n)) by B8;
then dom (G . n) = ((dom P) /\ (dom (F . n))) \ (((P " {-infty }) /\ ((F . n) " {+infty })) \/ ((P " {+infty }) /\ ((F . n) " {-infty }))) by MESFUNC1:def 3;
hence dom (G . n) = E by B4, B5, B61, A1; :: thesis:

end;

now

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

end;

then reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
B7: E = dom (G . 0 ) by B6;

now

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

now

let x be set ; :: thesis:
assume C11: x in dom (P + (F . n)) ; :: thesis:
then reconsider x1 = x as Element of X ;
x in E by C11, C10, B6;
then - (P . x) <= (F # x1) . n by A9;
then C12: - (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 C12, XXREAL_3:38;
hence 0 <= (P + (F . n)) . x by C11, MESFUNC1:def 3; :: thesis:

end;

hence G . n is nonnegative by C10, SUPINF_2:71; :: thesis:
F . n is_integrable_on M by A6;
then G . n is_integrable_on M by C10, A3, 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 B6; :: thesis:

end;

then consider IG being ExtREAL_sequence such that
C1: ( ( for n being Nat holds IG . n = Integral M,(G . n) ) & Integral M,(lim_inf G) <= lim_inf IG ) by B7, Th135;
( -infty < Integral M,P & Integral M,P < +infty ) by A3, MESFUNC5:102;
then C2: Integral M,P is Real by XXREAL_0:14;

now

let n be Nat; :: thesis:
( F . n is_integrable_on M & G . n = P + (F . n) ) by A6, B8;
then C31: 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 A3, MESFUNC5:115;
C32: dom (F . n) = E by A1, MESFUNC8:def 2;
then ( P | E = P & (F . n) | E = F . n ) by A1, RELAT_1:97;
then Integral M,(G . n) = (Integral M,P) + (I . n) by A1, C31, C32, B2;
hence IG . n = (Integral M,P) + (I . n) by C1; :: thesis:

end;

then C3: lim_inf IG = (Integral M,P) + (lim_inf I) by C2, limseq2;

now

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

now

let k be Nat; :: thesis:
k is Element of NAT by ORDINAL1:def 13;
then ( (inferior_realsequence (F # x)) . k <= (F # x) . k & (F # x) . k <= P . x ) by A9, C41, A7, RINFSUP2:8;
hence (inferior_realsequence (F # x)) . k <= P . x by XXREAL_0:2; :: thesis:

end;

then lim_inf (F # x) <= P . x by Th63b;
then C42: (lim_inf F) . x <= P . x by C41, MESFUNC8:def 8;

now

let y be ext-real number ; :: thesis:
assume y in rng (F # x) ; :: thesis:
then consider k being set such that
C43: ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 5;
thus - (P . x) <= y by C43, A9, C41, A7; :: 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 C44: - (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 C44, XXREAL_0:2;
then - (P . x) <= (lim_inf F) . x by C41, MESFUNC8:def 8;
hence |.((lim_inf F) . x).| <= P . x by C42, EXTREAL2:60; :: thesis:

end;

then lim_inf F is_integrable_on M by A7, A8, A1, A3, MESFUNC5:108;
then C4: 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 A3, MESFUNC5:115;
C5: ( -infty < Integral M,P & Integral M,P < +infty ) by A3, MESFUNC5:102;
( P | E = P & (lim_inf F) | E = lim_inf F & dom (G . 0 ) = dom (F . 0 ) ) by A1, A7, B6, RELAT_1:97;
then (Integral M,P) + (Integral M,(lim_inf F)) <= (Integral M,P) + (lim_inf I) by B8, C3, A1, A7, C4, C1, B4, B5, limfunc2;
then Integral M,(lim_inf F) <= ((lim_inf I) + (Integral M,P)) - (Integral M,P) by C5, XXREAL_3:67;
then Integral M,(lim_inf F) <= (lim_inf I) + ((Integral M,P) - (Integral M,P)) by C5, XXREAL_3:31;
then Integral M,(lim_inf F) <= (lim_inf I) + 0. by XXREAL_3:7;
then C6: Integral M,(lim_inf F) <= lim_inf I by XXREAL_3:4;
deffunc H₃( Element of NAT ) -> Element of K21(K22(X,ExtREAL )) = P - (F . $1);
consider H being Function such that
D1: ( dom H = NAT & ( for n being Element of NAT holds H . n = H₃(n) ) ) from FUNCT_1:sch 4();

D2: now

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

end;

now

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

end;

then reconsider H = H as Functional_Sequence of X,ExtREAL by D1, SEQFUNC:1;

D3: now

let n be natural number ; :: thesis:
( dom (F . n) = E & dom (H . n) = dom (P - (F . n)) ) by D2, A1, MESFUNC8:def 2;
then dom (H . n) = (E /\ E) \ (({} /\ ((F . n) " {+infty })) \/ ({} /\ ((F . n) " {-infty }))) by A1, B4, B5, MESFUNC1:def 4;
hence dom (H . n) = E ; :: thesis:

end;

now

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

end;

then reconsider H = H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;

D4: now

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

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 A9;
hence (F . n) . x <= P . x by MESFUNC5:def 13; :: thesis:

end;

hence H . n is nonnegative by D41, MESFUNC7:1; :: thesis:
F . n is_integrable_on M by A6;
then H . n is_integrable_on M by D41, A3, Th114a;
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 D3; :: thesis:

end;

E = dom (H . 0 ) by D3;
then consider IH being ExtREAL_sequence such that
D5: ( ( for n being Nat holds IH . n = Integral M,(H . n) ) & Integral M,(lim_inf H) <= lim_inf IH ) by D4, Th135;
deffunc H₄( Element of NAT ) -> Element of ExtREAL = - (I . $1);
consider I1 being Function of NAT ,ExtREAL such that
D6: for n being Element of NAT holds I1 . n = H₄(n) from FUNCT_2:sch 4();
reconsider I1 = I1 as ExtREAL_sequence ;

D7: now

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

end;

then D8: - (lim_inf I1) = lim_sup I by supinfa;

now

let n be Nat; :: thesis:
D91: ( F . n is_integrable_on M & H . n = P - (F . n) ) by D2, A6;
then D92: 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 A3, Th115a;
D93: dom (F . n) = E by A1, MESFUNC8:def 2;
then E = dom (- (F . n)) by MESFUNC1:def 7;
then D94: ( P | E = P & (- (F . n)) | E = - (F . n) ) by A1, RELAT_1:97;
Integral M,(- (F . n)) = Integral M,((- 1) (#) (F . n)) by MESFUNC2:11;
then D95: Integral M,(- (F . n)) = (R_EAL (- 1)) * (Integral M,(F . n)) by D91, MESFUNC5:116;
reconsider In = I . n as Real by B2;
( (R_EAL (- 1)) * (I . n) = (- 1) * In & - (I . n) = - In ) by EXTREAL1:13, SUPINF_2:3;
then Integral M,(H . n) = (Integral M,P) + (- (I . n)) by A1, B2, D92, D93, D94, D95;
then IH . n = (Integral M,P) + (- (I . n)) by D5;
hence IH . n = (Integral M,P) + (I1 . n) by D7; :: thesis:

end;

then D9: lim_inf IH = (Integral M,P) + (lim_inf I1) by C2, limseq2;
deffunc H₅( Element of NAT ) -> Element of K21(K22(X,ExtREAL )) = - (F . $1);
consider F1 being Function such that
E1: ( dom F1 = NAT & ( for n being Element of NAT holds F1 . n = H₅(n) ) ) from FUNCT_1:sch 4();

now

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

end;

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

E2: now

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

end;

now

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

end;

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;

E3: now

let n be Nat; :: thesis:
H . n = P - (F . n) by D2;
then H . n = P + (- (F . n)) by MESFUNC2:9;
hence H . n = P + (F1 . n) by E2; :: thesis:

end;

F1 . 0 = - (F . 0 ) by E2;
then E4: dom (F1 . 0 ) = dom (F . 0 ) by MESFUNC1:def 7;
then dom (F1 . 0 ) = dom (H . 0 ) by A1, D3;
then lim_inf H = P + (lim_inf F1) by E3, B4, B5, limfunc2;
then lim_inf H = P + (- (lim_sup F)) by E4, E2, supinfb;
then E5: lim_inf H = P - (lim_sup F) by MESFUNC2:9;

now

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

end;

then lim_sup (F # x) >= - (P . x) by Th63a;
then E62: (lim_sup F) . x >= - (P . x) by E61, MESFUNC8:def 9;

now

let y be ext-real number ; :: thesis:
assume y in rng (F # x) ; :: thesis:
then consider k being set such that
E63: ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 5;
thus P . x >= y by E63, A9, E61, A7; :: 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 E64: 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 E64, XXREAL_0:2;
then P . x >= (lim_sup F) . x by E61, MESFUNC8:def 9;
hence |.((lim_sup F) . x).| <= P . x by E62, EXTREAL2:60; :: thesis:

end;

then E6: lim_sup F is_integrable_on M by A7, A8, A1, A3, MESFUNC5:108;
then E7: 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 A3, Th115a;
E8: ( -infty < Integral M,P & Integral M,P < +infty ) by A3, MESFUNC5:102;
E = dom (lim_sup F) by A1, MESFUNC8:def 9;
then E = dom (- (lim_sup F)) by MESFUNC1:def 7;
then E9: ( P | E = P & (- (lim_sup F)) | E = - (lim_sup F) ) by A1, RELAT_1:97;
Integral M,(- (lim_sup F)) = Integral M,((- 1) (#) (lim_sup F)) by MESFUNC2:11;
then (Integral M,P) + ((R_EAL (- 1)) * (Integral M,(lim_sup F))) <= (Integral M,P) + (- (lim_sup I)) by D5, D9, D8, A1, A7, E5, E6, E7, E9, MESFUNC5:116;
then (R_EAL (- 1)) * (Integral M,(lim_sup F)) <= ((- (lim_sup I)) + (Integral M,P)) - (Integral M,P) by E8, XXREAL_3:67;
then (R_EAL (- 1)) * (Integral M,(lim_sup F)) <= (- (lim_sup I)) + ((Integral M,P) - (Integral M,P)) by E8, XXREAL_3:31;
then F1: (R_EAL (- 1)) * (Integral M,(lim_sup F)) <= (- (lim_sup I)) + 0. by XXREAL_3:7;
set E1 = Integral M,(lim_sup F);
( -infty < Integral M,(lim_sup F) & Integral M,(lim_sup F) < +infty ) by E6, MESFUNC5:102;
then reconsider e1 = Integral M,(lim_sup F) as Real by XXREAL_0:14;
( (R_EAL (- 1)) * (Integral M,(lim_sup F)) = (- 1) * e1 & - (Integral M,(lim_sup F)) = - e1 ) by EXTREAL1:13, SUPINF_2:3;
then - (Integral M,(lim_sup F)) <= - (lim_sup I) by F1, XXREAL_3:4;
then F2: Integral M,(lim_sup F) >= lim_sup I by XXREAL_3:40;

now

assume L1: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
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;
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 Integral M,(lim F) <= lim_inf I by C6, L3, PARTFUN1:34;
then L7: lim_sup I <= lim_inf I by L5, F2, 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, C6, F2, 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 B2, C6, F2; :: thesis: