let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let g be PartFunc of X,ExtREAL ; :: thesis:
let F be Functional_Sequence of X,ExtREAL ; :: thesis:
let L be ExtREAL_sequence; :: thesis:
assume that
A1: g is_simple_func_in S and
A2: for x being set st x in dom g holds
0 < g . x and
A3: for n being Nat holds F . n is_simple_func_in S and
A4: for n being Nat holds dom (F . n) = dom g and
A5: for n being Nat holds F . n is nonnegative and
A6: for n, m being Nat st n <= m holds
for x being Element of X st x in dom g holds
(F . n) . x <= (F . m) . x and
A7: for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) and
A8: for n being Nat holds L . n = integral' M,(F . n) ; :: thesis:

suppose A9: dom g = {} ; :: thesis:

A10: now

let n be Nat; :: thesis:
dom (F . n) = {} by A4, A9;
then integral' M,(F . n) = 0 by Def14;
hence L . n = R_EAL 0 by A8; :: thesis:

end;

then L is convergent_to_finite_number by Th58;
hence L is convergent by Def11; :: thesis:
lim L = R_EAL 0 by A10, Th58;
hence integral' M,g <= lim L by A9, Def14; :: thesis:

end;

suppose A11: dom g <> {} ; :: thesis:

for v being set st v in dom g holds
0 <= g . v by A2;
then consider G being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A12: G,a are_Re-presentation_of g and
A13: a . 1 = 0 and
A14: for n being Nat st 2 <= n & n in dom a holds
( 0 < a . n & a . n < +infty ) by A1, MESFUNC3:14;
defpred S₁[ Nat, set ] means $2 = a . $1;
A15: for k being Nat st k in Seg (len a) holds
ex x being Element of REAL st S₁[k,x]

proof

let k be Nat; :: thesis:
assume A16: k in Seg (len a) ; :: thesis:
then A17: 1 <= k by FINSEQ_1:3;
A18: k in dom a by A16, FINSEQ_1:def 3;

per cases ;

suppose A19: k = 1 ; :: thesis:

take x = 0 ; :: thesis:
thus S₁[k,x] by A13, A19; :: thesis:

end;

suppose k <> 1 ; :: thesis:

then k > 1 by A17, XXREAL_0:1;
then A20: k >= 1 + 1 by NAT_1:13;
then A21: a . k < +infty by A14, A18;
0 < a . k by A14, A18, A20;
then reconsider x = a . k as Element of REAL by A21, XXREAL_0:14;
take x ; :: thesis:
thus S₁[k,x] ; :: thesis:

end;

consider a1 being FinSequence of REAL such that
A22: ( dom a1 = Seg (len a) & ( for k being Nat st k in Seg (len a) holds
S₁[k,a1 . k] ) ) from FINSEQ_1:sch 5(A15);
A23: len a <> 0

proof

assume len a = 0 ; :: thesis:
then A24: dom a = Seg 0 by FINSEQ_1:def 3;
A25: rng G = {}

proof

assume rng G <> {} ; :: thesis:
then consider y being set such that
A26: y in rng G by XBOOLE_0:def 1;
ex x being set st
( x in dom G & y = G . x ) by A26, FUNCT_1:def 5;
hence contradiction by A12, A24, MESFUNC3:def 1; :: thesis:

end;

union (rng G) <> {} by A11, A12, MESFUNC3:def 1;
then consider x being set such that
A27: x in union (rng G) by XBOOLE_0:def 1;
ex Y being set st
( x in Y & Y in rng G ) by A27, TARSKI:def 4;
hence contradiction by A25; :: thesis:

end;

A28: 2 <= len a

proof

assume not 2 <= len a ; :: thesis:
then len a = 1 by A23, NAT_1:23;
then dom a = {1} by FINSEQ_1:4, FINSEQ_1:def 3;
then A29: dom G = {1} by A12, MESFUNC3:def 1;
A30: dom g = union (rng G) by A12, MESFUNC3:def 1
.= union {(G . 1)} by A29, FUNCT_1:14
.= G . 1 by ZFMISC_1:31 ;
then consider x being set such that
A31: x in G . 1 by A11, XBOOLE_0:def 1;
1 in dom G by A29, TARSKI:def 1;
then g . x = 0 by A12, A13, A31, MESFUNC3:def 1;
hence contradiction by A2, A30, A31; :: thesis:

end;

then 1 <= len a by XXREAL_0:2;
then 1 in Seg (len a) ;
then A32: a . 1 = a1 . 1 by A22;
A33: 2 in dom a1 by A22, A28;
then A34: 2 in dom a by A22, FINSEQ_1:def 3;
a1 . 2 = a . 2 by A22, A33;
then a1 . 2 <> a . 1 by A13, A14, A34;
then A35: not a1 . 2 in {(a1 . 1)} by A32, TARSKI:def 1;
a1 . 2 in rng a1 by A33, FUNCT_1:12;
then reconsider RINGA = (rng a1) \ {(a1 . 1)} as non empty finite real-membered set by A35, XBOOLE_0:def 5;
set alpha = R_EAL (min RINGA);
reconsider beta1 = max RINGA as Real by XREAL_0:def 1;
A36: min RINGA in RINGA by XXREAL_2:def 7;
then min RINGA in rng a1 by XBOOLE_0:def 5;
then consider i being set such that
A37: i in dom a1 and
A38: min RINGA = a1 . i by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A37;
A39: a . i = R_EAL (a1 . i) by A22, A37;
i in Seg (len a1) by A37, FINSEQ_1:def 3;
then A40: 1 <= i by FINSEQ_1:3;
not min RINGA in {(a1 . 1)} by A36, XBOOLE_0:def 5;
then i <> 1 by A38, TARSKI:def 1;
then 1 < i by A40, XXREAL_0:1;
then A41: 1 + 1 <= i by NAT_1:13;
A42: i in dom a by A22, A37, FINSEQ_1:def 3;
then A43: 0 < R_EAL (min RINGA) by A14, A38, A41, A39;
set beta = R_EAL (max RINGA);
A44: for x being set st x in dom g holds
( R_EAL (min RINGA) <= g . x & g . x <= R_EAL (max RINGA) )

proof

let x be set ; :: thesis:
assume A45: x in dom g ; :: thesis:
then x in union (rng G) by A12, MESFUNC3:def 1;
then consider Y being set such that
A46: x in Y and
A47: Y in rng G by TARSKI:def 4;
consider k being set such that
A48: k in dom G and
A49: Y = G . k by A47, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A48;
k in dom a by A12, A48, MESFUNC3:def 1;
then A50: k in Seg (len a) by FINSEQ_1:def 3;

now

1 <= len a by A28, XXREAL_0:2;
then A51: 1 in dom a1 by A22;
A52: g . x = a . k by A12, A46, A48, A49, MESFUNC3:def 1;
assume A53: a1 . k = a1 . 1 ; :: thesis:
a . k = a1 . k by A22, A50;
then a . k = a . 1 by A22, A53, A51;
hence contradiction by A2, A13, A45, A52; :: thesis:

end;

then A54: not a1 . k in {(a1 . 1)} by TARSKI:def 1;
a1 . k in rng a1 by A22, A50, FUNCT_1:12;
then A55: a1 . k in RINGA by A54, XBOOLE_0:def 5;
g . x = a . k by A12, A46, A48, A49, MESFUNC3:def 1
.= a1 . k by A22, A50 ;
hence ( R_EAL (min RINGA) <= g . x & g . x <= R_EAL (max RINGA) ) by A55, XXREAL_2:def 7, XXREAL_2:def 8; :: thesis:

end;

A56: for n being Nat holds dom (g - (F . n)) = dom g

proof

g is without-infty by A1, Th20;
then not -infty in rng g by Def3;
then A57: g " {-infty } = {} by FUNCT_1:142;
g is without+infty by A1, Th20;
then not +infty in rng g by Def4;
then A58: g " {+infty } = {} by FUNCT_1:142;
let n be Nat; :: thesis:
A59: dom (g - (F . n)) = ((dom (F . n)) /\ (dom g)) \ ((((F . n) " {+infty }) /\ (g " {+infty })) \/ (((F . n) " {-infty }) /\ (g " {-infty }))) by MESFUNC1:def 4;
dom (F . n) = dom g by A4;
hence dom (g - (F . n)) = dom g by A58, A57, A59; :: thesis:

end;

A60: g is V55() by A1, MESFUNC2:def 5;
A61: for e being R_eal st R_EAL 0 < e & e < R_EAL (min RINGA) holds
ex H being SetSequence of X ex MF being ExtREAL_sequence st
( ( for n being Nat holds H . n = less_dom (g - (F . n)),e ) & ( for n, m being Nat st n <= m holds
H . n c= H . m ) & ( for n being Nat holds H . n c= dom g ) & ( for n being Nat holds MF . n = M . (H . n) ) & M . (dom g) = sup (rng MF) & ( for n being Nat holds H . n in S ) )

proof

let e be R_eal; :: thesis:
assume that
A62: R_EAL 0 < e and
A63: e < R_EAL (min RINGA) ; :: thesis:
deffunc H₁( Nat) -> Element of bool X = less_dom (g - (F . $1)),e;
consider H being SetSequence of X such that
A64: for n being Element of NAT holds H . n = H₁(n) from FUNCT_2:sch 4();

A65: now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence H . n = H₁(n) by A64; :: thesis:

end;

A66: for n being Nat holds H . n c= dom g

proof

let n be Nat; :: thesis:

now

let x be set ; :: thesis:
assume x in H . n ; :: thesis:
then x in less_dom (g - (F . n)),e by A65;
then x in dom (g - (F . n)) by MESFUNC1:def 12;
hence x in dom g by A56; :: thesis:

end;

hence H . n c= dom g by TARSKI:def 3; :: thesis:

end;

A67: Union H c= dom g

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Union H ; :: thesis:
then consider n being Element of NAT such that
A68: x in H . n by PROB_1:25;
H . n c= dom g by A66;
hence x in dom g by A68; :: thesis:

end;

now

let x be set ; :: thesis:
assume A69: x in dom g ; :: thesis:
then reconsider x1 = x as Element of X ;
A70: F # x1 is convergent by A7, A69;

A71: now

reconsider E = e as Real by A62, A63, XXREAL_0:48;
assume F # x1 is convergent_to_-infty ; :: thesis:
then consider N being Nat such that
A72: for m being Nat st N <= m holds
(F # x1) . m <= R_EAL (- E) by A62, Def10;
F . N is nonnegative by A5;
then A73: 0 <= (F . N) . x by SUPINF_2:70;
(F # x1) . N < 0 by A62, A72;
hence contradiction by A73, Def13; :: thesis:

end;

now

per cases by A70, A71, Def11;

suppose A74: F # x1 is convergent_to_finite_number ; :: thesis:

reconsider E = e as Real by A62, A63, XXREAL_0:48;
A75: ( ex limFx being real number st
( lim (F # x1) = limFx & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((F # x1) . m) - (lim (F # x1))).| < p ) & F # x1 is convergent_to_finite_number ) or ( lim (F # x1) = +infty & F # x1 is convergent_to_+infty ) or ( lim (F # x1) = -infty & F # x1 is convergent_to_-infty ) ) by A70, Def12;
then consider N being Nat such that
A76: for m being Nat st N <= m holds
|.(((F # x1) . m) - (lim (F # x1))).| < R_EAL (E / 2) by A62, A74, Th56, Th57;
reconsider N = N as Element of NAT by ORDINAL1:def 13;
g . x <= lim (F # x1) by A7, A69;
then (g . x) - (R_EAL (E / 2)) <= (lim (F # x1)) - 0. by A62, XXREAL_3:39;
then A77: (g . x) - (R_EAL (E / 2)) <= lim (F # x1) by XXREAL_3:4;

now

let k be Element of NAT ; :: thesis:
set m = N + k;
A78: x1 in dom (g - (F . (N + k))) by A56, A69;

now

let e be real number ; :: thesis:
assume 0 < e ; :: thesis:
then consider N0 being Nat such that
A79: for M being Nat st N0 <= M holds
|.(((F # x1) . M) - (lim (F # x1))).| < R_EAL e by A74, A75, Th56, Th57;
reconsider N0 = N0, n1 = N + k as Element of NAT by ORDINAL1:def 13;
set M = max N0,n1;
A80: ((F # x1) . (max N0,n1)) - (lim (F # x1)) <= |.(((F # x1) . (max N0,n1)) - (lim (F # x1))).| by EXTREAL2:57;
(F . (N + k)) . x1 <= (F . (max N0,n1)) . x1 by A6, A69, XXREAL_0:25;
then (F . (N + k)) . x1 <= (F # x1) . (max N0,n1) by Def13;
then A81: (F # x1) . (N + k) <= (F # x1) . (max N0,n1) by Def13;
|.(((F # x1) . (max N0,n1)) - (lim (F # x1))).| < R_EAL e by A79, XXREAL_0:25;
then ((F # x1) . (max N0,n1)) - (lim (F # x1)) < R_EAL e by A80, XXREAL_0:2;
then (F # x1) . (max N0,n1) < (R_EAL e) + (lim (F # x1)) by A74, A75, Th56, Th57, XXREAL_3:65;
hence (F # x1) . (N + k) < (lim (F # x1)) + e by A81, XXREAL_0:2; :: thesis:

end;

then (F # x1) . (N + k) <= lim (F # x1) by XXREAL_3:72;
then A82: 0 <= (lim (F # x1)) - ((F # x1) . (N + k)) by XXREAL_3:43;
|.(((F # x1) . (N + k)) - (lim (F # x1))).| = |.((lim (F # x1)) - ((F # x1) . (N + k))).| by Th1
.= (lim (F # x1)) - ((F # x1) . (N + k)) by A82, EXTREAL1:def 3 ;
then (lim (F # x1)) - ((F # x1) . (N + k)) < R_EAL (E / 2) by A76, NAT_1:11;
then A83: (lim (F # x1)) - ((F . (N + k)) . x1) < R_EAL (E / 2) by Def13;
A84: |.(((F # x1) . (N + k)) - (lim (F # x1))).| < R_EAL (E / 2) by A76, NAT_1:11;
then (F # x1) . (N + k) <> -infty by A74, A75, Th3, Th57;
then A85: (F . (N + k)) . x <> -infty by Def13;
(F # x1) . (N + k) <> +infty by A74, A75, A84, Th3, Th56;
then (F . (N + k)) . x <> +infty by Def13;
then lim (F # x1) < ((F . (N + k)) . x) + (R_EAL (E / 2)) by A85, A83, XXREAL_3:65;
then A86: (lim (F # x1)) + (E / 2) < (((F . (N + k)) . x) + (R_EAL (E / 2))) + (E / 2) by XXREAL_3:73;
g . x <= (lim (F # x1)) + (R_EAL (E / 2)) by A77, XXREAL_3:44;
then g . x < (((F . (N + k)) . x1) + (R_EAL (E / 2))) + (R_EAL (E / 2)) by A86, XXREAL_0:2;
then g . x < ((F . (N + k)) . x1) + ((R_EAL (E / 2)) + (R_EAL (E / 2))) by XXREAL_3:30;
then g . x < ((F . (N + k)) . x1) + (R_EAL ((E / 2) + (E / 2))) by SUPINF_2:1;
then (g . x) - ((F . (N + k)) . x1) < e by XXREAL_3:66;
then (g - (F . (N + k))) . x1 < e by A78, MESFUNC1:def 4;
then x in less_dom (g - (F . (N + k))),e by A78, MESFUNC1:def 12;
hence x in H . (N + k) by A65; :: thesis:

end;

then A87: x in (inferior_setsequence H) . N by SETLIM_1:19;
dom (inferior_setsequence H) = NAT by FUNCT_2:def 1;
hence ex N being Nat st
( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N ) by A87; :: thesis:

end;

suppose A88: F # x1 is convergent_to_+infty ; :: thesis:

ex N being Nat st
for m being Nat st N <= m holds
(g . x1) - ((F . m) . x1) < e

proof

A89: e in REAL by A62, A63, XXREAL_0:48;

per cases ) - e <= 0 or 0 < (g . x1) - e ) ;

suppose A90: (g . x1) - e <= 0 ; :: thesis:

consider N being Nat such that
A91: for m being Nat st N <= m holds
R_EAL 1 <= (F # x1) . m by A88, Def9;

now

let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then (g . x1) - e < (F # x1) . m by A90, A91;
then g . x1 < ((F # x1) . m) + e by A89, XXREAL_3:65;
then (g . x1) - ((F # x1) . m) < e by A89, XXREAL_3:66;
hence (g . x1) - ((F . m) . x1) < e by Def13; :: thesis:

end;

hence ex N being Nat st
for m being Nat st N <= m holds
(g . x1) - ((F . m) . x1) < e ; :: thesis:

end;

suppose A92: 0 < (g . x1) - e ; :: thesis:

reconsider e1 = e as Real by A62, A63, XXREAL_0:48;
reconsider gx1 = g . x as Real by A60, XXREAL_0:14;
(g . x) - e = gx1 - e1 by SUPINF_2:5;
then reconsider ee = (g . x1) - e as Real ;
consider N being Nat such that
A93: for m being Nat st N <= m holds
R_EAL (ee + 1) <= (F # x1) . m by A88, A92, Def9;
A94: R_EAL ee < R_EAL (ee + 1) by XREAL_1:31;

now

let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then R_EAL (ee + 1) <= (F # x1) . m by A93;
then R_EAL ee < (F # x1) . m by A94, XXREAL_0:2;
then g . x1 < ((F # x1) . m) + e by A89, XXREAL_3:65;
then (g . x1) - ((F # x1) . m) < e by A89, XXREAL_3:66;
hence (g . x1) - ((F . m) . x1) < e by Def13; :: thesis:

end;

hence ex N being Nat st
for m being Nat st N <= m holds
(g . x1) - ((F . m) . x1) < e ; :: thesis:

end;

then consider N being Nat such that
A95: for m being Nat st N <= m holds
(g . x1) - ((F . m) . x1) < e ;
reconsider N = N as Element of NAT by ORDINAL1:def 13;

A96: now

let m be Nat; :: thesis:
A97: x1 in dom (g - (F . m)) by A56, A69;
assume N <= m ; :: thesis:
then (g . x1) - ((F . m) . x1) < e by A95;
then (g - (F . m)) . x1 < e by A97, MESFUNC1:def 4;
hence x1 in less_dom (g - (F . m)),e by A97, MESFUNC1:def 12; :: thesis:

end;

now

let k be Element of NAT ; :: thesis:
x in less_dom (g - (F . (N + k))),e by A96, NAT_1:11;
hence x in H . (N + k) by A65; :: thesis:

end;

then A98: x in (inferior_setsequence H) . N by SETLIM_1:19;
dom (inferior_setsequence H) = NAT by FUNCT_2:def 1;
hence ex N being Nat st
( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N ) by A98; :: thesis:

end;

then consider N being Nat such that
A99: N in dom (inferior_setsequence H) and
A100: x in (inferior_setsequence H) . N ;
(inferior_setsequence H) . N in rng (inferior_setsequence H) by A99, FUNCT_1:12;
then x in Union (inferior_setsequence H) by A100, TARSKI:def 4;
hence x in lim_inf H by SETLIM_1:def 4; :: thesis:

end;

then A101: dom g c= lim_inf H by TARSKI:def 3;
deffunc H₂( Nat) -> Element of ExtREAL = M . (H . $1);
A102: lim_inf H c= lim_sup H by KURATO_2:9;
consider MF being ExtREAL_sequence such that
A103: for n being Element of NAT holds MF . n = H₂(n) from FUNCT_2:sch 4();
A104: for n, m being Nat st n <= m holds
H . n c= H . m

proof

let n, m be Nat; :: thesis:
assume A105: n <= m ; :: thesis:

now

let x be set ; :: thesis:
assume x in H . n ; :: thesis:
then A106: x in less_dom (g - (F . n)),e by A65;
then A107: x in dom (g - (F . n)) by MESFUNC1:def 12;
then A108: (g - (F . n)) . x = (g . x) - ((F . n) . x) by MESFUNC1:def 4;
A109: (g - (F . n)) . x < e by A106, MESFUNC1:def 12;
A110: dom (g - (F . n)) = dom g by A56;
then A111: (F . n) . x <= (F . m) . x by A6, A105, A107;
A112: dom (g - (F . m)) = dom g by A56;
then (g - (F . m)) . x = (g . x) - ((F . m) . x) by A107, A110, MESFUNC1:def 4;
then (g - (F . m)) . x <= (g - (F . n)) . x by A108, A111, XXREAL_3:39;
then (g - (F . m)) . x < e by A109, XXREAL_0:2;
then x in less_dom (g - (F . m)),e by A107, A110, A112, MESFUNC1:def 12;
hence x in H . m by A65; :: thesis:

end;

hence H . n c= H . m by TARSKI:def 3; :: thesis:

end;

then for n, m being Element of NAT st n <= m holds
H . n c= H . m ;
then A113: H is non-descending by PROB_1:def 7;

A114: now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence MF . n = H₂(n) by A103; :: thesis:

end;

now

let x be set ; :: thesis:
assume x in lim_inf H ; :: thesis:
then x in Union (inferior_setsequence H) by SETLIM_1:def 4;
then consider V being set such that
A115: x in V and
A116: V in rng (inferior_setsequence H) by TARSKI:def 4;
consider n being set such that
A117: n in dom (inferior_setsequence H) and
A118: V = (inferior_setsequence H) . n by A116, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A117;
x in H . (n + 0 ) by A115, A118, SETLIM_1:19;
then x in less_dom (g - (F . n)),e by A65;
then x in dom (g - (F . n)) by MESFUNC1:def 12;
hence x in dom g by A56; :: thesis:

end;

then lim_inf H c= dom g by TARSKI:def 3;
then A119: lim_inf H = dom g by A101, XBOOLE_0:def 10;
A120: ( M . (dom g) = sup (rng MF) & ( for n being Element of NAT holds H . n in S ) )

proof

A121: now

reconsider E = e as Real by A62, A63, XXREAL_0:48;
let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
A122: less_dom (g - (F . n)),(R_EAL E) c= dom (g - (F . n))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in less_dom (g - (F . n)),(R_EAL E) ; :: thesis:
hence x in dom (g - (F . n)) by MESFUNC1:def 12; :: thesis:

end;

A123: F . n is_simple_func_in S by A3;
then consider GF being Finite_Sep_Sequence of S such that
A124: dom (F . n) = union (rng GF) and
for m being Nat
for x, y being Element of X st m in dom GF & x in GF . m & y in GF . m holds
(F . n) . x = (F . n) . y by MESFUNC2:def 5;
A125: F . n is V55() by A123, MESFUNC2:def 5;
reconsider DGH = union (rng GF) as Element of S by MESFUNC2:34;
dom (F . n) = dom g by A4;
then DGH /\ (less_dom (g - (F . n)),(R_EAL E)) = (dom (g - (F . n))) /\ (less_dom (g - (F . n)),(R_EAL E)) by A56, A124;
then A126: DGH /\ (less_dom (g - (F . n)),(R_EAL E)) = less_dom (g - (F . n)),(R_EAL E) by A122, XBOOLE_1:28;
A127: F . n is_measurable_on DGH by A3, MESFUNC2:37;
A128: g is V55() by A1, MESFUNC2:def 5;
g is_measurable_on DGH by A1, MESFUNC2:37;
then g - (F . n) is_measurable_on DGH by A124, A128, A125, A127, MESFUNC2:13;
then DGH /\ (less_dom (g - (F . n)),(R_EAL E)) in S by MESFUNC1:def 17;
hence H . x in S by A65, A126; :: thesis:

end;

dom H = NAT by FUNCT_2:def 1;
then reconsider HH = H as Function of NAT ,S by A121, FUNCT_2:5;
A129: for n being Element of NAT holds HH . n c= HH . (n + 1) by A104, NAT_1:11;
rng HH c= S by RELAT_1:def 19;
then A130: rng H c= dom M by FUNCT_2:def 1;
lim_sup H = Union H by A113, SETLIM_1:59;
then A131: M . (union (rng H)) = M . (dom g) by A119, A67, A102, XBOOLE_0:def 10;
A132: dom H = NAT by FUNCT_2:def 1;
A133: dom MF = NAT by FUNCT_2:def 1;
A134: for x being set holds
( x in dom MF iff ( x in dom H & H . x in dom M ) )

proof

let x be set ; :: thesis:

now

assume A135: x in dom MF ; :: thesis:
then H . x in rng H by A132, FUNCT_1:12;
hence ( x in dom H & H . x in dom M ) by A132, A130, A135; :: thesis:

end;

hence ( x in dom MF iff ( x in dom H & H . x in dom M ) ) by A133; :: thesis:

end;

for x being set st x in dom MF holds
MF . x = M . (H . x) by A103;
then M * H = MF by A134, FUNCT_1:20;
hence ( M . (dom g) = sup (rng MF) & ( for n being Element of NAT holds H . n in S ) ) by A121, A129, A131, MEASURE2:27; :: thesis:

end;

now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence H . n in S by A120; :: thesis:

end;

hence ex H being SetSequence of X ex MF being ExtREAL_sequence st
( ( for n being Nat holds H . n = less_dom (g - (F . n)),e ) & ( for n, m being Nat st n <= m holds
H . n c= H . m ) & ( for n being Nat holds H . n c= dom g ) & ( for n being Nat holds MF . n = M . (H . n) ) & M . (dom g) = sup (rng MF) & ( for n being Nat holds H . n in S ) ) by A65, A104, A66, A114, A120; :: thesis:

end;

per cases ;

suppose A136: M . (dom g) <> +infty ; :: thesis:

A137: 0 < R_EAL (max RINGA)

proof

consider x being set such that
A138: x in dom g by A11, XBOOLE_0:def 1;
A139: g . x <= R_EAL (max RINGA) by A44, A138;
R_EAL (min RINGA) <= g . x by A44, A138;
hence 0 < R_EAL (max RINGA) by A14, A38, A41, A42, A39, A139; :: thesis:

end;

A140: {} in S by MEASURE1:66;
A141: M . {} = 0 by VALUED_0:def 19;
dom g is Element of S by A1, Th43;
then A142: M . (dom g) <> -infty by A141, A140, MEASURE1:62, XBOOLE_1:2;
then reconsider MG = M . (dom g) as Real by A136, XXREAL_0:14;
reconsider DG = dom g as Element of S by A1, Th43;
A143: for x being set st x in dom g holds
0 <= g . x by A2;
then A144: integral' M,g <> -infty by A1, Th74, SUPINF_2:71;
A145: g is nonnegative by A143, SUPINF_2:71;
A146: integral' M,g <= (R_EAL (max RINGA)) * (M . DG)

proof

consider GP being PartFunc of X,ExtREAL such that
A147: GP is_simple_func_in S and
A148: dom GP = DG and
A149: for x being set st x in DG holds
GP . x = R_EAL (max RINGA) by Th47;
A150: for x being set st x in dom (GP - g) holds
g . x <= GP . x

proof

let x be set ; :: thesis:
assume x in dom (GP - g) ; :: thesis:
then x in ((dom GP) /\ (dom g)) \ (((GP " {+infty }) /\ (g " {+infty })) \/ ((GP " {-infty }) /\ (g " {-infty }))) by MESFUNC1:def 4;
then A151: x in (dom GP) /\ (dom g) by XBOOLE_0:def 5;
then GP . x = R_EAL (max RINGA) by A148, A149;
hence g . x <= GP . x by A44, A148, A151; :: thesis:

end;

for x being set st x in dom GP holds
0 <= GP . x by A137, A148, A149;
then A152: GP is nonnegative by SUPINF_2:71;
then A153: dom (GP - g) = (dom GP) /\ (dom g) by A1, A145, A147, A150, Th75;
then A154: g | (dom (GP - g)) = g by A148, GRFUNC_1:64;
A155: GP | (dom (GP - g)) = GP by A148, A153, GRFUNC_1:64;
integral' M,(g | (dom (GP - g))) <= integral' M,(GP | (dom (GP - g))) by A1, A145, A147, A152, A150, Th76;
hence integral' M,g <= (R_EAL (max RINGA)) * (M . DG) by A137, A147, A148, A149, A154, A155, Th77; :: thesis:

end;

(R_EAL (max RINGA)) * (M . DG) = beta1 * MG by EXTREAL1:13;
then A156: integral' M,g <> +infty by A146, XXREAL_0:9;
A157: for e being R_eal st 0 < e & e < R_EAL (min RINGA) holds
ex N0 being Nat st
for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n)

proof

let e be R_eal; :: thesis:
assume that
A158: 0 < e and
A159: e < R_EAL (min RINGA) ; :: thesis:
A160: e <> +infty by A159, XXREAL_0:4;
consider H being SetSequence of X, MF being ExtREAL_sequence such that
A161: for n being Nat holds H . n = less_dom (g - (F . n)),e and
A162: for n, m being Nat st n <= m holds
H . n c= H . m and
A163: for n being Nat holds H . n c= dom g and
A164: for n being Nat holds MF . n = M . (H . n) and
A165: M . (dom g) = sup (rng MF) and
A166: for n being Nat holds H . n in S by A61, A158, A159;
sup (rng MF) is Real by A136, A142, A165, XXREAL_0:14;
then consider y being ext-real number such that
A167: y in rng MF and
A168: (sup (rng MF)) - e < y by A158, MEASURE6:33;
consider N0 being set such that
A169: N0 in dom MF and
A170: y = MF . N0 by A167, FUNCT_1:def 5;
reconsider N0 = N0 as Element of NAT by A169;
reconsider B0 = H . N0 as Element of S by A166;
M . B0 <= M . DG by A163, MEASURE1:62;
then M . B0 < +infty by A136, XXREAL_0:2, XXREAL_0:4;
then A171: M . (DG \ B0) = (M . DG) - (M . B0) by A163, MEASURE1:63;
take N0 ; :: thesis:
(M . (dom g)) - e < M . (H . N0) by A164, A165, A168, A170;
then M . (dom g) < (M . (H . N0)) + e by A158, A160, XXREAL_3:65;
then A172: (M . (dom g)) - (M . (H . N0)) < e by A158, A160, XXREAL_3:66;

A173: now

let n be Nat; :: thesis:
reconsider BN = H . n as Element of S by A166;
assume N0 <= n ; :: thesis:
then H . N0 c= H . n by A162;
then M . (DG \ BN) <= M . (DG \ B0) by MEASURE1:62, XBOOLE_1:34;
hence M . ((dom g) \ (H . n)) < e by A172, A171, XXREAL_0:2; :: thesis:

end;

now

reconsider XSMg = integral' M,g as Real by A156, A144, XXREAL_0:14;
let n be Nat; :: thesis:
A174: for x being set st x in dom (F . n) holds
(F . n) . x = (F . n) . x ;
reconsider B = H . n as Element of S by A166;
H . n in S by A166;
then X \ (H . n) in S by MEASURE1:66;
then A175: DG /\ (X \ (H . n)) in S by MEASURE1:66;
DG /\ (X \ (H . n)) = (DG /\ X) \ (H . n) by XBOOLE_1:49;
then reconsider A = DG \ (H . n) as Element of S by A175, XBOOLE_1:28;
e <> +infty by A159, XXREAL_0:4;
then reconsider ee = e as Real by A158, XXREAL_0:14;
A176: A misses B by XBOOLE_1:79;
(R_EAL (max RINGA)) * e = beta1 * ee by EXTREAL1:13;
then reconsider betae = (R_EAL (max RINGA)) * e as Real ;
A177: for x being set st x in dom g holds
g . x = g . x ;
A178: M . B <= M . DG by A163, MEASURE1:62;
then M . (dom g) <> -infty by A141, A140, MEASURE1:62, XBOOLE_1:2;
then A179: M . (dom g) is Real by A136, XXREAL_0:14;
A180: DG = DG \/ (H . n) by A163, XBOOLE_1:12;
then A181: DG = (DG \ (H . n)) \/ (H . n) by XBOOLE_1:39;
then dom g = (A \/ B) /\ (dom g) ;
then g = g | (A \/ B) by A177, FUNCT_1:68;
then A182: integral' M,g = (integral' M,(g | A)) + (integral' M,(g | B)) by A1, A145, Th73, XBOOLE_1:79;
M . A <= M . DG by A181, MEASURE1:62, XBOOLE_1:7;
then M . A < +infty by A136, XXREAL_0:2, XXREAL_0:4;
then (R_EAL (max RINGA)) * (M . A) < (R_EAL (max RINGA)) * +infty by A137, XXREAL_3:83;
then A183: (R_EAL (max RINGA)) * (M . A) <> +infty by A137, XXREAL_3:def 5;
A184: g | B is nonnegative by A143, Th21, SUPINF_2:71;
A185: dom (F . n) = dom g by A4;
then dom (F . n) = (A \/ B) /\ (dom (F . n)) by A181;
then A186: F . n = (F . n) | (A \/ B) by A174, FUNCT_1:68;
consider GP being PartFunc of X,ExtREAL such that
A187: GP is_simple_func_in S and
A188: dom GP = A and
A189: for x being set st x in A holds
GP . x = R_EAL (max RINGA) by Th47;
A190: integral' M,GP = (R_EAL (max RINGA)) * (M . A) by A137, A187, A188, A189, Th77;
A191: dom (g | A) = A by A181, RELAT_1:91, XBOOLE_1:7;
A192: for x being set st x in dom (GP - (g | A)) holds
(g | A) . x <= GP . x

proof

let x be set ; :: thesis:
assume x in dom (GP - (g | A)) ; :: thesis:
then x in ((dom GP) /\ (dom (g | A))) \ (((GP " {+infty }) /\ ((g | A) " {+infty })) \/ ((GP " {-infty }) /\ ((g | A) " {-infty }))) by MESFUNC1:def 4;
then A193: x in (dom GP) /\ (dom (g | A)) by XBOOLE_0:def 5;
then A194: x in dom GP by XBOOLE_0:def 4;
x in (dom g) /\ A by A191, A188, A193, RELAT_1:90;
then x in dom g by XBOOLE_0:def 4;
then A195: g . x <= R_EAL (max RINGA) by A44;
(g | A) . x = g . x by A191, A188, A193, FUNCT_1:70;
hence (g | A) . x <= GP . x by A188, A189, A194, A195; :: thesis:

end;

for x being set st x in dom GP holds
0 <= GP . x by A137, A188, A189;
then A196: GP is nonnegative by SUPINF_2:71;
0 <= M . A by A141, A140, MEASURE1:62, XBOOLE_1:2;
then reconsider XSMGP = integral' M,GP as Real by A137, A190, A183, XXREAL_0:14;
A197: (integral' M,g) - (integral' M,GP) = XSMg - XSMGP by SUPINF_2:5;
A198: g | A is_simple_func_in S by A1, Th40;
then A199: integral' M,(g | A) <> -infty by A145, Th21, Th74;
A200: g | A is nonnegative by A143, Th21, SUPINF_2:71;
then A201: dom (GP - (g | A)) = (dom GP) /\ (dom (g | A)) by A198, A187, A196, A192, Th75;
then A202: GP | (dom (GP - (g | A))) = GP by A191, A188, GRFUNC_1:64;
(g | A) | (dom (GP - (g | A))) = g | A by A191, A188, A201, GRFUNC_1:64;
then A203: integral' M,(g | A) <= integral' M,GP by A198, A200, A187, A196, A192, A202, Th76;
then A204: (integral' M,g) - (integral' M,GP) <= (integral' M,g) - (integral' M,(g | A)) by XXREAL_3:39;
assume N0 <= n ; :: thesis:
then M . A < e by A173;
then A205: (R_EAL (max RINGA)) * (M . A) < (R_EAL (max RINGA)) * e by A137, XXREAL_3:83;
then A206: integral' M,(g | A) <> +infty by A203, A190, XXREAL_0:2, XXREAL_0:4;
then reconsider XSMgA = integral' M,(g | A) as Real by A199, XXREAL_0:14;
A207: integral' M,(g | A) is Element of REAL by A199, A206, XXREAL_0:14;
XSMg - XSMgA = (integral' M,g) - (integral' M,(g | A)) by SUPINF_2:5
.= integral' M,(g | B) by A182, A207, XXREAL_3:24 ;
then reconsider XSMgB = integral' M,(g | B) as Real ;
A208: H . n c= DG by A163;
integral' M,(g | A) is Element of REAL by A199, A206, XXREAL_0:14;
then A209: (integral' M,g) - (integral' M,(g | A)) = integral' M,(g | B) by A182, XXREAL_3:24;
XSMg - betae < XSMg - XSMGP by A190, A205, XREAL_1:17;
then A210: XSMg - betae < XSMgB by A209, A204, A197, XXREAL_0:2;
consider EP being PartFunc of X,ExtREAL such that
A211: EP is_simple_func_in S and
A212: dom EP = B and
A213: for x being set st x in B holds
EP . x = e by A158, A160, Th47;
A214: integral' M,EP = e * (M . B) by A158, A211, A212, A213, Th77;
for x being set st x in dom EP holds
0 <= EP . x by A158, A212, A213;
then A215: EP is nonnegative by SUPINF_2:71;
M . B < +infty by A136, A178, XXREAL_0:2, XXREAL_0:4;
then e * (M . B) < e * +infty by A158, A160, XXREAL_3:83;
then A216: integral' M,EP <> +infty by A214, XXREAL_0:4;
A217: 0 <= M . B by A141, A140, MEASURE1:62, XBOOLE_1:2;
then reconsider XSMEP = integral' M,EP as Real by A158, A214, A216, XXREAL_0:14;
A218: F . n is_simple_func_in S by A3;
(F . n) | A is nonnegative by A5, Th21;
then A219: 0 <= integral' M,((F . n) | A) by A218, Th40, Th74;
F . n is nonnegative by A5;
then integral' M,(F . n) = (integral' M,((F . n) | A)) + (integral' M,((F . n) | B)) by A3, A186, A176, Th73;
then A220: integral' M,((F . n) | B) <= integral' M,(F . n) by A219, XXREAL_3:42;
A221: M . (dom g) < +infty by A136, XXREAL_0:4;
M . B <> -infty by A141, A140, MEASURE1:62, XBOOLE_1:2;
then M . B is Real by A221, A178, XXREAL_0:14;
then consider MB, MG being Real such that
A222: MB = M . B and
A223: MG = M . (dom g) and
A224: MB <= MG by A208, A179, MEASURE1:62;
A225: g | B is_simple_func_in S by A1, Th40;
ee * MB <= ee * MG by A158, A224, XREAL_1:66;
then A226: (XSMg - betae) - (ee * MG) <= (XSMg - betae) - (ee * MB) by XREAL_1:15;
XSMEP = e * (M . B) by A158, A211, A212, A213, Th77
.= ee * MB by A222, EXTREAL1:13 ;
then A227: (XSMg - betae) - (ee * MB) < XSMgB - XSMEP by A210, XREAL_1:16;
betae = ee * beta1 by EXTREAL1:13;
then A228: XSMg - (ee * (beta1 + MG)) < XSMgB - XSMEP by A227, A226, XXREAL_0:2;
dom ((F . n) | B) = (dom (F . n)) /\ B by RELAT_1:90;
then A229: dom ((F . n) | B) = B by A163, A185, XBOOLE_1:28;
A230: (F . n) | B is_simple_func_in S by A3, Th40;
then A231: ((F . n) | B) + EP is_simple_func_in S by A211, Th44;
A232: (F . n) | B is nonnegative by A5, Th21;
then A233: dom (((F . n) | B) + EP) = (dom ((F . n) | B)) /\ (dom EP) by A230, A211, A215, Th71;
A234: dom (((F . n) | B) + EP) = (dom ((F . n) | B)) /\ (dom EP) by A232, A230, A211, A215, Th71
.= B by A229, A212 ;
A235: dom (g | B) = B by A180, RELAT_1:91, XBOOLE_1:7;
A236: for x being set st x in dom ((((F . n) | B) + EP) - (g | B)) holds
(g | B) . x <= (((F . n) | B) + EP) . x

proof

set f = g - (F . n);
let x be set ; :: thesis:
assume x in dom ((((F . n) | B) + EP) - (g | B)) ; :: thesis:
then x in ((dom (((F . n) | B) + EP)) /\ (dom (g | B))) \ ((((((F . n) | B) + EP) " {+infty }) /\ ((g | B) " {+infty })) \/ (((((F . n) | B) + EP) " {-infty }) /\ ((g | B) " {-infty }))) by MESFUNC1:def 4;
then A237: x in (dom (((F . n) | B) + EP)) /\ (dom (g | B)) by XBOOLE_0:def 5;
then A238: x in dom (((F . n) | B) + EP) by XBOOLE_0:def 4;
then (((F . n) | B) + EP) . x = (((F . n) | B) . x) + (EP . x) by MESFUNC1:def 3;
then (((F . n) | B) + EP) . x = ((F . n) . x) + (EP . x) by A229, A234, A238, FUNCT_1:70;
then A239: (((F . n) | B) + EP) . x = ((F . n) . x) + e by A213, A234, A238;
A240: x in less_dom (g - (F . n)),e by A161, A234, A238;
then A241: (g - (F . n)) . x < e by MESFUNC1:def 12;
x in dom (g - (F . n)) by A240, MESFUNC1:def 12;
then A242: (g . x) - ((F . n) . x) <= e by A241, MESFUNC1:def 4;
(g | B) . x = g . x by A235, A234, A237, FUNCT_1:70;
hence (g | B) . x <= (((F . n) | B) + EP) . x by A158, A160, A239, A242, XXREAL_3:44; :: thesis:

end;

A243: ((F . n) | B) + EP is nonnegative by A232, A215, Th25;
then A244: dom ((((F . n) | B) + EP) - (g | B)) = (dom (((F . n) | B) + EP)) /\ (dom (g | B)) by A225, A184, A231, A236, Th75;
then A245: g | B = (g | B) | (dom ((((F . n) | B) + EP) - (g | B))) by A229, A212, A235, A233, GRFUNC_1:64;
((F . n) | B) + EP = (((F . n) | B) + EP) | (dom ((((F . n) | B) + EP) - (g | B))) by A229, A212, A235, A244, A233, GRFUNC_1:64;
then A246: integral' M,(g | B) <= integral' M,(((F . n) | B) + EP) by A225, A184, A231, A243, A236, A245, Th76;
integral' M,(((F . n) | B) + EP) = (integral' M,(((F . n) | B) | B)) + (integral' M,(EP | B)) by A232, A230, A211, A215, A234, Th71
.= (integral' M,(((F . n) | B) | B)) + (integral' M,EP) by A212, GRFUNC_1:64
.= (integral' M,((F . n) | B)) + (integral' M,EP) by FUNCT_1:82 ;
then A247: (integral' M,(g | B)) - (integral' M,EP) <= integral' M,((F . n) | B) by A158, A214, A217, A216, A246, XXREAL_3:45;
beta1 + MG = (R_EAL (max RINGA)) + (M . (dom g)) by A223, SUPINF_2:1;
then ee * (beta1 + MG) = e * ((R_EAL (max RINGA)) + (M . (dom g))) by EXTREAL1:13;
then A248: XSMg - (ee * (beta1 + MG)) = (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) by SUPINF_2:5;
XSMgB - XSMEP = (integral' M,(g | B)) - (integral' M,EP) by SUPINF_2:5;
then (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,((F . n) | B) by A247, A228, A248, XXREAL_0:2;
hence (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) by A220, XXREAL_0:2; :: thesis:

end;

hence for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) ; :: thesis:

end;

A249: for e being R_eal st 0 < e & e < R_EAL (min RINGA) holds
ex N0 being Nat st
for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < L . n

proof

let e be R_eal; :: thesis:
assume that
A250: 0 < e and
A251: e < R_EAL (min RINGA) ; :: thesis:
consider N0 being Nat such that
A252: for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) by A157, A250, A251;

now

let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) by A252;
hence (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < L . n by A8; :: thesis:

end;

hence ex N0 being Nat st
for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < L . n ; :: thesis:

end;

A253: for e1 being R_eal st 0 < e1 holds
ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 )

proof

reconsider ralpha = R_EAL (min RINGA) as Real by XXREAL_0:14;
reconsider rdomg = M . (dom g) as Real by A136, A142, XXREAL_0:14;
let e1 be R_eal; :: thesis:
assume A254: 0 < e1 ; :: thesis:
{} c= DG by XBOOLE_1:2;
then A255: 0 <= rdomg by A141, A140, MEASURE1:62;

per cases ;

suppose A256: e1 = +infty ; :: thesis:

set z = ralpha / 2;
(R_EAL (ralpha / 2)) * ((R_EAL (max RINGA)) + (M . (dom g))) <= +infty by XXREAL_0:4;
hence ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 ) by A43, A256, XREAL_1:218; :: thesis:

end;

suppose e1 <> +infty ; :: thesis:

then reconsider re1 = e1 as Real by A254, XXREAL_0:14;
set x = re1 / (beta1 + rdomg);
set y = ralpha / 2;
set z = min (re1 / (beta1 + rdomg)),(ralpha / 2);
A257: min (re1 / (beta1 + rdomg)),(ralpha / 2) <= ralpha / 2 by XXREAL_0:17;
ralpha / 2 < ralpha by A43, XREAL_1:218;
then A258: min (re1 / (beta1 + rdomg)),(ralpha / 2) < ralpha by A257, XXREAL_0:2;
R_EAL (beta1 + rdomg) = (R_EAL beta1) + (R_EAL rdomg) by SUPINF_2:1;
then A259: (min (re1 / (beta1 + rdomg)),(ralpha / 2)) * (beta1 + rdomg) = (R_EAL (min (re1 / (beta1 + rdomg)),(ralpha / 2))) * ((R_EAL (max RINGA)) + (M . (dom g))) by EXTREAL1:38;

A260: now

per cases by XXREAL_0:15;

suppose min (re1 / (beta1 + rdomg)),(ralpha / 2) = re1 / (beta1 + rdomg) ; :: thesis:

hence 0 < min (re1 / (beta1 + rdomg)),(ralpha / 2) by A137, A254, A255; :: thesis:

end;

suppose min (re1 / (beta1 + rdomg)),(ralpha / 2) = ralpha / 2 ; :: thesis:

hence 0 < min (re1 / (beta1 + rdomg)),(ralpha / 2) by A43; :: thesis:

end;

(min (re1 / (beta1 + rdomg)),(ralpha / 2)) * (beta1 + rdomg) <= (re1 / (beta1 + rdomg)) * (beta1 + rdomg) by A137, A255, XREAL_1:66, XXREAL_0:17;
then (min (re1 / (beta1 + rdomg)),(ralpha / 2)) * (beta1 + rdomg) <= re1 by A137, A255, XCMPLX_1:88;
hence ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 ) by A260, A258, A259; :: thesis:

end;

A261: for e1 being R_eal st 0 < e1 holds
ex N0 being Nat st
for n being Nat st N0 <= n holds
(integral' M,g) - e1 < L . n

proof

let e1 be R_eal; :: thesis:
assume 0 < e1 ; :: thesis:
then consider e being R_eal such that
A262: 0 < e and
A263: e < R_EAL (min RINGA) and
A264: e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 by A253;
consider N0 being Nat such that
A265: for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < L . n by A249, A262, A263;
take N0 ; :: thesis:

now

let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then A266: (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < L . n by A265;
(integral' M,g) - e1 <= (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) by A264, XXREAL_3:39;
hence (integral' M,g) - e1 < L . n by A266, XXREAL_0:2; :: thesis:

end;

hence for n being Nat st N0 <= n holds
(integral' M,g) - e1 < L . n ; :: thesis:

end;

A267: for n being Nat holds 0 <= L . n

proof

let n be Nat; :: thesis:
F . n is nonnegative by A5;
then 0 <= integral' M,(F . n) by A3, Th74;
hence 0 <= L . n by A8; :: thesis:

end;

A268: for n, m being Nat st n <= m holds
L . n <= L . m

proof

let n, m be Nat; :: thesis:
A269: dom (F . n) = dom g by A4;
A270: F . m is_simple_func_in S by A3;
A271: dom (F . m) = dom g by A4;
assume A272: n <= m ; :: thesis:
A273: for x being set st x in dom ((F . m) - (F . n)) holds
(F . n) . x <= (F . m) . x

proof

let x be set ; :: thesis:
assume x in dom ((F . m) - (F . n)) ; :: thesis:
then x in ((dom (F . m)) /\ (dom (F . n))) \ ((((F . m) " {+infty }) /\ ((F . n) " {+infty })) \/ (((F . m) " {-infty }) /\ ((F . n) " {-infty }))) by MESFUNC1:def 4;
then x in (dom (F . m)) /\ (dom (F . n)) by XBOOLE_0:def 5;
hence (F . n) . x <= (F . m) . x by A6, A272, A269, A271; :: thesis:

end;

A274: F . n is_simple_func_in S by A3;
A275: F . m is nonnegative by A5;
A276: F . n is nonnegative by A5;
then A277: dom ((F . m) - (F . n)) = (dom (F . m)) /\ (dom (F . n)) by A275, A274, A270, A273, Th75;
then A278: (F . m) | (dom ((F . m) - (F . n))) = F . m by A269, A271, GRFUNC_1:64;
A279: (F . n) | (dom ((F . m) - (F . n))) = F . n by A269, A271, A277, GRFUNC_1:64;
integral' M,((F . n) | (dom ((F . m) - (F . n)))) <= integral' M,((F . m) | (dom ((F . m) - (F . n)))) by A276, A275, A274, A270, A273, Th76;
then L . n <= integral' M,(F . m) by A8, A278, A279;
hence L . n <= L . m by A8; :: thesis:

end;

per cases ;

suppose ex K being real number st
( 0 < K & ( for n being Nat holds L . n < K ) ) ; :: thesis:

then consider K being real number such that
0 < K and
A280: for n being Nat holds L . n < K ;

now

let x be ext-real number ; :: thesis:
assume x in rng L ; :: thesis:
then ex z being set st
( z in dom L & x = L . z ) by FUNCT_1:def 5;
hence x <= R_EAL K by A280; :: thesis:

end;

then R_EAL K is UpperBound of rng L by XXREAL_2:def 1;
then A281: sup (rng L) <= R_EAL K by XXREAL_2:def 3;
R_EAL K is Real by XREAL_0:def 1;
then A282: sup (rng L) <> +infty by A281, XXREAL_0:9;
A283: for n being Nat holds L . n <= sup (rng L)

proof

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;
dom L = NAT by FUNCT_2:def 1;
then A284: L . n in rng L by FUNCT_1:def 5;
sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;
hence L . n <= sup (rng L) by A284, XXREAL_2:def 1; :: thesis:

end;

then L . 1 <= sup (rng L) ;
then A285: sup (rng L) <> -infty by A267;
then reconsider h = sup (rng L) as Real by A282, XXREAL_0:14;
A286: for p being real number st 0 < p holds
ex N0 being Nat st
for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p

proof

let p be real number ; :: thesis:
assume A287: 0 < p ; :: thesis:
A288: sup (rng L) <> (sup (rng L)) + (R_EAL p)

proof

assume A289: sup (rng L) = (sup (rng L)) + (R_EAL p) ; :: thesis:
((R_EAL p) + (sup (rng L))) + (- (sup (rng L))) = (R_EAL p) + ((sup (rng L)) + (- (sup (rng L)))) by A285, A282, XXREAL_3:30
.= (R_EAL p) + 0 by XXREAL_3:7
.= R_EAL p by XXREAL_3:4 ;
hence contradiction by A287, A289, XXREAL_3:7; :: thesis:

end;

sup (rng L) is Real by A285, A282, XXREAL_0:14;
then consider y being ext-real number such that
A290: y in rng L and
A291: (sup (rng L)) - (R_EAL p) < y by A287, MEASURE6:33;
consider x being set such that
A292: x in dom L and
A293: y = L . x by A290, FUNCT_1:def 5;
reconsider N0 = x as Element of NAT by A292;
take N0 ; :: thesis:
let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then L . N0 <= L . n by A268;
then (sup (rng L)) - (R_EAL p) < L . n by A291, A293, XXREAL_0:2;
then sup (rng L) < (L . n) + (R_EAL p) by XXREAL_3:65;
then (sup (rng L)) - (L . n) < R_EAL p by XXREAL_3:66;
then - (R_EAL p) < - ((sup (rng L)) - (L . n)) by XXREAL_3:40;
then A294: - (R_EAL p) < (L . n) - (sup (rng L)) by XXREAL_3:27;
A295: L . n <= sup (rng L) by A283;
(sup (rng L)) + 0. <= (sup (rng L)) + (R_EAL p) by A287, XXREAL_3:38;
then sup (rng L) <= (sup (rng L)) + (R_EAL p) by XXREAL_3:4;
then sup (rng L) < (sup (rng L)) + (R_EAL p) by A288, XXREAL_0:1;
then L . n < (sup (rng L)) + (R_EAL p) by A295, XXREAL_0:2;
then (L . n) - (sup (rng L)) < R_EAL p by XXREAL_3:66;
hence |.((L . n) - (sup (rng L))).| < p by A294, EXTREAL2:59; :: thesis:

end;

A296: R_EAL h = sup (rng L) ;
then A297: L is convergent_to_finite_number by A286, Def8;
hence L is convergent by Def11; :: thesis:
then A298: lim L = sup (rng L) by A286, A296, A297, Def12;

now

let e be real number ; :: thesis:
assume 0 < e ; :: thesis:
then consider N0 being Nat such that
A299: for n being Nat st N0 <= n holds
(integral' M,g) - (R_EAL e) < L . n by A261;
A300: L . N0 <= sup (rng L) by A283;
(integral' M,g) - (R_EAL e) < L . N0 by A299;
then (integral' M,g) - (R_EAL e) < sup (rng L) by A300, XXREAL_0:2;
hence integral' M,g < (lim L) + e by A298, XXREAL_3:65; :: thesis:

end;

hence integral' M,g <= lim L by XXREAL_3:72; :: thesis:

end;

suppose A301: for K being real number holds
( not 0 < K or ex n being Nat st not L . n < K ) ; :: thesis:

now

let K be real number ; :: thesis:
assume 0 < K ; :: thesis:
then consider N0 being Nat such that
A302: R_EAL K <= L . N0 by A301;

now

let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then L . N0 <= L . n by A268;
hence R_EAL K <= L . n by A302, XXREAL_0:2; :: thesis:

end;

hence ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n ; :: thesis:

end;

then A303: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis:
then lim L = +infty by A303, Def12;
hence integral' M,g <= lim L by XXREAL_0:4; :: thesis:

end;

suppose A304: M . (dom g) = +infty ; :: thesis:

reconsider DG = dom g as Element of S by A1, Th43;
A305: for e being R_eal st 0 < e & e < R_EAL (min RINGA) holds
for n being Nat holds ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n)

proof

let e be R_eal; :: thesis:
assume that
A306: 0 < e and
A307: e < R_EAL (min RINGA) ; :: thesis:
A308: 0 <= (R_EAL (min RINGA)) - e by A307, XXREAL_3:43;
consider H being SetSequence of X, MF being ExtREAL_sequence such that
A309: for n being Nat holds H . n = less_dom (g - (F . n)),e and
for n, m being Nat st n <= m holds
H . n c= H . m and
A310: for n being Nat holds H . n c= dom g and
for n being Nat holds MF . n = M . (H . n) and
M . (dom g) = sup (rng MF) and
A311: for n being Nat holds H . n in S by A61, A306, A307;
A312: e <> +infty by A307, XXREAL_0:4;

now

let n be Nat; :: thesis:
reconsider B = H . n as Element of S by A311;
A313: for x being set st x in dom (F . n) holds
(F . n) . x = (F . n) . x ;
H . n in S by A311;
then A314: X \ (H . n) in S by MEASURE1:66;
DG /\ (X \ (H . n)) = (DG /\ X) \ (H . n) by XBOOLE_1:49
.= DG \ (H . n) by XBOOLE_1:28 ;
then reconsider A = DG \ (H . n) as Element of S by A314, MEASURE1:66;
A315: dom (F . n) = dom g by A4;
A316: DG = DG \/ (H . n) by A310, XBOOLE_1:12
.= (DG \ (H . n)) \/ (H . n) by XBOOLE_1:39 ;
then dom (F . n) = (A \/ B) /\ (dom (F . n)) by A315;
then A317: F . n = (F . n) | (A \/ B) by A313, FUNCT_1:68;
consider EP being PartFunc of X,ExtREAL such that
A318: EP is_simple_func_in S and
A319: dom EP = B and
A320: for x being set st x in B holds
EP . x = (R_EAL (min RINGA)) - e by A306, A308, Th47, XXREAL_3:18;
for x being set st x in dom EP holds
0 <= EP . x by A308, A319, A320;
then A321: EP is nonnegative by SUPINF_2:71;
A322: dom ((F . n) | B) = (dom (F . n)) /\ B by RELAT_1:90
.= B by A316, A315, XBOOLE_1:7, XBOOLE_1:28 ;
A323: for x being set st x in dom (((F . n) | B) - EP) holds
EP . x <= ((F . n) | B) . x

proof

set f = g - (F . n);
let x be set ; :: thesis:
assume x in dom (((F . n) | B) - EP) ; :: thesis:
then x in ((dom ((F . n) | B)) /\ (dom EP)) \ (((((F . n) | B) " {+infty }) /\ (EP " {+infty })) \/ ((((F . n) | B) " {-infty }) /\ (EP " {-infty }))) by MESFUNC1:def 4;
then A324: x in (dom ((F . n) | B)) /\ (dom EP) by XBOOLE_0:def 5;
then A325: x in dom ((F . n) | B) by XBOOLE_0:def 4;
then A326: ((F . n) | B) . x = (F . n) . x by FUNCT_1:70;
A327: x in less_dom (g - (F . n)),e by A309, A322, A325;
then A328: x in dom (g - (F . n)) by MESFUNC1:def 12;
(g - (F . n)) . x < e by A327, MESFUNC1:def 12;
then (g . x) - ((F . n) . x) <= e by A328, MESFUNC1:def 4;
then g . x <= ((F . n) . x) + e by A306, A312, XXREAL_3:44;
then A329: (g . x) - e <= (F . n) . x by A306, A312, XXREAL_3:45;
dom (g - (F . n)) = dom g by A56;
then R_EAL (min RINGA) <= g . x by A44, A328;
then (R_EAL (min RINGA)) - e <= (g . x) - e by XXREAL_3:39;
then (R_EAL (min RINGA)) - e <= (F . n) . x by A329, XXREAL_0:2;
hence EP . x <= ((F . n) | B) . x by A322, A319, A320, A324, A326; :: thesis:

end;

A330: F . n is_simple_func_in S by A3;
(F . n) | A is nonnegative by A5, Th21;
then A331: 0 <= integral' M,((F . n) | A) by A330, Th40, Th74;
A332: A misses B by XBOOLE_1:79;
F . n is nonnegative by A5;
then integral' M,(F . n) = (integral' M,((F . n) | A)) + (integral' M,((F . n) | B)) by A3, A317, A332, Th73;
then A333: integral' M,((F . n) | B) <= integral' M,(F . n) by A331, XXREAL_3:42;
A334: (F . n) | B is_simple_func_in S by A3, Th40;
A335: (F . n) | B is nonnegative by A5, Th21;
then A336: dom (((F . n) | B) - EP) = (dom ((F . n) | B)) /\ (dom EP) by A334, A318, A321, A323, Th75;
then A337: EP | (dom (((F . n) | B) - EP)) = EP by A322, A319, GRFUNC_1:64;
A338: ((F . n) | B) | (dom (((F . n) | B) - EP)) = (F . n) | B by A322, A319, A336, GRFUNC_1:64;
integral' M,(EP | (dom (((F . n) | B) - EP))) <= integral' M,(((F . n) | B) | (dom (((F . n) | B) - EP))) by A335, A334, A318, A321, A323, Th76;
then A339: integral' M,EP <= integral' M,(F . n) by A333, A337, A338, XXREAL_0:2;
integral' M,EP = ((R_EAL (min RINGA)) - e) * (M . B) by A307, A318, A319, A320, Th77, XXREAL_3:43;
hence ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n) by A309, A339; :: thesis:

end;

hence for n being Nat holds ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n) ; :: thesis:

end;

for y being real number st 0 < y holds
ex n being Nat st
for m being Nat st n <= m holds
y <= L . m

proof

reconsider ralpha = R_EAL (min RINGA) as Real by XXREAL_0:14;
set e = (R_EAL (min RINGA)) / (R_EAL 2);
let y be real number ; :: thesis:
assume 0 < y ; :: thesis:
set a2 = ralpha / 2;
reconsider y1 = y as Real by XREAL_0:def 1;
y = (ralpha - (ralpha / 2)) * (y1 / (ralpha - (ralpha / 2))) by A43, XCMPLX_1:88;
then A340: y = (R_EAL (ralpha - (ralpha / 2))) * (R_EAL (y1 / (ralpha - (ralpha / 2)))) by EXTREAL1:38;
A341: (R_EAL (min RINGA)) / (R_EAL 2) = ralpha / 2 by EXTREAL1:39;
then consider H being SetSequence of X, MF being ExtREAL_sequence such that
A342: for n being Nat holds H . n = less_dom (g - (F . n)),((R_EAL (min RINGA)) / (R_EAL 2)) and
A343: for n, m being Nat st n <= m holds
H . n c= H . m and
for n being Nat holds H . n c= dom g and
A344: for n being Nat holds MF . n = M . (H . n) and
A345: M . (dom g) = sup (rng MF) and
A346: for n being Nat holds H . n in S by A61, A43, XREAL_1:218;
y / (ralpha - (ralpha / 2)) = (R_EAL y1) / (R_EAL (ralpha - (ralpha / 2))) by EXTREAL1:39
.= (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) by A341, SUPINF_2:5 ;
then A347: (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) < +infty by XXREAL_0:9;
ex z being ext-real number st
( z in rng MF & (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) <= z )

proof

assume for z being ext-real number holds
( not z in rng MF or not (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) <= z ) ; :: thesis:
then for z being ext-real number st z in rng MF holds
z <= (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) ;
then (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) is UpperBound of rng MF by XXREAL_2:def 1;
hence contradiction by A304, A347, A345, XXREAL_2:def 3; :: thesis:

end;

then consider z being R_eal such that
A348: z in rng MF and
A349: (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) <= z ;
(ralpha / 2) - (ralpha / 2) < ralpha - (ralpha / 2) by A43;
then A350: 0 < (R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2)) by A341, SUPINF_2:5;
consider x being set such that
A351: x in dom MF and
A352: z = MF . x by A348, FUNCT_1:def 5;
reconsider N0 = x as Element of NAT by A351;
take N0 ; :: thesis:
(R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2)) = ralpha - (ralpha / 2) by A341, SUPINF_2:5;
then A353: ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * ((R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2)))) = y by A340, EXTREAL1:39;
thus for m being Nat st N0 <= m holds
y <= L . m :: thesis:

proof

(R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) <= M . (H . N0) by A344, A349, A352;
then A354: R_EAL y <= ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (H . N0)) by A350, A353, XXREAL_3:82;
let m be Nat; :: thesis:
A355: H . m in S by A346;
assume N0 <= m ; :: thesis:
then A356: H . N0 c= H . m by A343;
H . N0 in S by A346;
then ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (H . N0)) <= ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (H . m)) by A350, A356, A355, MEASURE1:62, XXREAL_3:82;
then R_EAL y <= ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (H . m)) by A354, XXREAL_0:2;
then A357: R_EAL y <= ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (less_dom (g - (F . m)),((R_EAL (min RINGA)) / (R_EAL 2)))) by A342;
((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (less_dom (g - (F . m)),((R_EAL (min RINGA)) / (R_EAL 2)))) <= integral' M,(F . m) by A43, A305, A341, XREAL_1:218;
then R_EAL y <= integral' M,(F . m) by A357, XXREAL_0:2;
hence y <= L . m by A8; :: thesis:

end;

then A358: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis:
then ( ex g being real number st
( lim L = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (lim L)).| < p ) & L is convergent_to_finite_number ) or ( lim L = +infty & L is convergent_to_+infty ) or ( lim L = -infty & L is convergent_to_-infty ) ) by Def12;
hence integral' M,g <= lim L by A358, Th56, XXREAL_0:4; :: thesis:

end;