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

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

end;

then L is convergent_to_finite_number by Th52;
hence L is convergent ; :: thesis:
lim L = 0 by A10, Th52;
hence integral' (M,g) <= lim L by A9, Def14; :: thesis:

end;

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

for v being object st v in dom g holds
0 <= g . v by A2;
then g is nonnegative by SUPINF_2:52;
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:1;
A18: k in dom a by A16, FINSEQ_1:def 3;

per cases ;

suppose A19: k = 1 ; :: thesis:

take In (0,REAL) ; :: thesis:
thus S₁[k, In (0,REAL)] 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 object such that
A26: y in rng G by XBOOLE_0:def 1;
ex x being object st
( x in dom G & y = G . x ) by A26, FUNCT_1:def 3;
hence contradiction by A12, A24, MESFUNC3:def 1; :: thesis:

end;

union (rng G) <> {} by A11, A12, MESFUNC3:def 1;
then consider x being object 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:2, 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:4
.= G . 1 by ZFMISC_1:25 ;
then consider x being object 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:3;
then reconsider RINGA = (rng a1) \ {(a1 . 1)} as non empty finite real-membered set by A35, XBOOLE_0:def 5;
reconsider alpha = min RINGA as R_eal by XXREAL_0:def 1;
reconsider beta1 = max RINGA as Element of 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 object such that
A37: i in dom a1 and
A38: min RINGA = a1 . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A37;
A39: a . i = a1 . i by A22, A37;
i in Seg (len a1) by A37, FINSEQ_1:def 3;
then A40: 1 <= i by FINSEQ_1:1;
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 < alpha by A14, A38, A41, A39;
reconsider beta = max RINGA as R_eal by XXREAL_0:def 1;
A44: for x being set st x in dom g holds
( alpha <= g . x & g . x <= beta )

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 object such that
A48: k in dom G and
A49: Y = G . k by A47, FUNCT_1:def 3;
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 :: thesis:

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:3;
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 ( alpha <= g . x & g . x <= beta ) 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 () by A1, Th14;
then not -infty in rng g ;
then A57: g " {-infty} = {} by FUNCT_1:72;
g is () by A1, Th14;
then not +infty in rng g ;
then A58: g " {+infty} = {} by FUNCT_1:72;
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 real-valued by A1, MESFUNC2:def 4;
A61: for e being R_eal st 0 < e & e < alpha 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: 0 < e and
A63: e < alpha ; :: 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 :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
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 :: thesis:

let x be object ; :: 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 11;
hence x in dom g by A56; :: thesis:

end;

hence H . n c= dom g ; :: thesis:

end;

A67: Union H c= dom g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union H ; :: thesis:
then consider n being Nat such that
A68: x in H . n by PROB_1:12;
H . n c= dom g by A66;
hence x in dom g by A68; :: thesis:

end;

now :: thesis:

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

reconsider E = e as Element of 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 <= - E by A62;
F . N is nonnegative by A5;
then A73: 0 <= (F . N) . x by SUPINF_2:51;
(F # x1) . N < 0 by A62, A72;
hence contradiction by A73, Def13; :: thesis:

end;

now :: thesis:

per cases by A70, A71;

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

reconsider E = e as Element of REAL by A62, A63, XXREAL_0:48;
A75: ( ex limFx being Real st
( lim (F # x1) = limFx & ( for p being Real 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))).| < E / 2 by A62, A74, Th50, Th51;
reconsider N = N as Element of NAT by ORDINAL1:def 12;
g . x <= lim (F # x1) by A7, A69;
then (g . x) - (E / 2) <= (lim (F # x1)) - 0. by A62, XXREAL_3:37;
then A77: (g . x) - (E / 2) <= lim (F # x1) by XXREAL_3:4;

now :: thesis:

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

now :: thesis:

let e be Real; :: 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))).| < e by A74, A75, Th50, Th51;
reconsider N0 = N0, n1 = N + k as Element of NAT by ORDINAL1:def 12;
set M = max (N0,n1);
A80: ((F # x1) . (max (N0,n1))) - (lim (F # x1)) <= |.(((F # x1) . (max (N0,n1))) - (lim (F # x1))).| by EXTREAL1:20;
(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))).| < e by A79, XXREAL_0:25;
then ((F # x1) . (max (N0,n1))) - (lim (F # x1)) < e by A80, XXREAL_0:2;
then (F # x1) . (max (N0,n1)) < e + (lim (F # x1)) by A74, A75, Th50, Th51, XXREAL_3:54;
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:61;
then A82: 0 <= (lim (F # x1)) - ((F # x1) . (N + k)) by XXREAL_3:40;
|.(((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 1 ;
then (lim (F # x1)) - ((F # x1) . (N + k)) < E / 2 by A76, NAT_1:11;
then A83: (lim (F # x1)) - ((F . (N + k)) . x1) < E / 2 by Def13;
A84: |.(((F # x1) . (N + k)) - (lim (F # x1))).| < E / 2 by A76, NAT_1:11;
then (F # x1) . (N + k) <> -infty by A74, A75, Th3, Th51;
then A85: (F . (N + k)) . x <> -infty by Def13;
(F # x1) . (N + k) <> +infty by A74, A75, A84, Th3, Th50;
then (F . (N + k)) . x <> +infty by Def13;
then lim (F # x1) < ((F . (N + k)) . x) + (E / 2) by A85, A83, XXREAL_3:54;
then A86: (lim (F # x1)) + (E / 2) < (((F . (N + k)) . x) + (E / 2)) + (E / 2) by XXREAL_3:62;
g . x <= (lim (F # x1)) + (E / 2) by A77, XXREAL_3:41;
then g . x < (((F . (N + k)) . x1) + (E / 2)) + (E / 2) by A86, XXREAL_0:2;
then g . x < ((F . (N + k)) . x1) + ((E / 2) + (E / 2)) by XXREAL_3:29;
then g . x < ((F . (N + k)) . x1) + ((E / 2) + (E / 2)) ;
then (g . x) - ((F . (N + k)) . x1) < e by XXREAL_3:55;
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 11;
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
1 <= (F # x1) . m by A88;

now :: thesis:

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:54;
then (g . x1) - ((F # x1) . m) < e by A89, XXREAL_3:55;
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 Element of REAL by A62, A63, XXREAL_0:48;
reconsider gx1 = g . x as Real by A60;
(g . x) - e = gx1 - e1 ;
then reconsider ee = (g . x1) - e as Real ;
consider N being Nat such that
A93: for m being Nat st N <= m holds
ee + 1 <= (F # x1) . m by A88, A92;
A94: ee < ee + 1 by XREAL_1:29;

now :: thesis:

let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then ee + 1 <= (F # x1) . m by A93;
then ee < (F # x1) . m by A94, XXREAL_0:2;
then g . x1 < ((F # x1) . m) + e by A89, XXREAL_3:54;
then (g . x1) - ((F # x1) . m) < e by A89, XXREAL_3:55;
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 12;

A96: now :: thesis:

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

end;

now :: thesis:

let k be 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:3;
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 ;
deffunc H₂( Nat) -> Element of ExtREAL = M . (H . $1);
A102: lim_inf H c= lim_sup H by KURATO_0:6;
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 :: thesis:

let x be object ; :: 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 11;
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 11;
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:37;
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 11;
hence x in H . m by A65; :: thesis:

end;

hence H . n c= H . m ; :: thesis:

end;

then for n, m being Nat st n <= m holds
H . n c= H . m ;
then A113: H is non-descending by PROB_1:def 5;

A114: now :: thesis:

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

end;

now :: thesis:

let x be object ; :: 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 object such that
A117: n in dom (inferior_setsequence H) and
A118: V = (inferior_setsequence H) . n by A116, FUNCT_1:def 3;
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 11;
hence x in dom g by A56; :: thesis:

end;

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

proof

A121: now :: thesis:

reconsider E = e as Element of REAL by A62, A63, XXREAL_0:48;
let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
A122: less_dom ((g - (F . n)),E) c= dom (g - (F . n)) by MESFUNC1:def 11;
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 4;
A125: F . n is real-valued by A123, MESFUNC2:def 4;
reconsider DGH = union (rng GF) as Element of S by MESFUNC2:31;
dom (F . n) = dom g by A4;
then DGH /\ (less_dom ((g - (F . n)),E)) = (dom (g - (F . n))) /\ (less_dom ((g - (F . n)),E)) by A56, A124;
then A126: DGH /\ (less_dom ((g - (F . n)),E)) = less_dom ((g - (F . n)),E) by A122, XBOOLE_1:28;
A127: F . n is DGH -measurable by A3, MESFUNC2:34;
A128: g is real-valued by A1, MESFUNC2:def 4;
g is DGH -measurable by A1, MESFUNC2:34;
then g - (F . n) is DGH -measurable by A124, A128, A125, A127, MESFUNC2:11;
then DGH /\ (less_dom ((g - (F . n)),E)) in S by MESFUNC1:def 16;
hence H . x in S by A65, A126; :: thesis:

end;

dom H = NAT by FUNCT_2:def 1;
then reconsider HH = H as sequence of S by A121, FUNCT_2:3;
A129: for n being 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 object holds
( x in dom MF iff ( x in dom H & H . x in dom M ) )

proof

let x be object ; :: thesis:

now :: thesis:

assume A135: x in dom MF ; :: thesis:
then H . x in rng H by A132, FUNCT_1:3;
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 object st x in dom MF holds
MF . x = M . (H . x) by A103;
then M * H = MF by A134, FUNCT_1:10;
hence ( M . (dom g) = sup (rng MF) & ( for n being Element of NAT holds H . n in S ) ) by A121, A129, A131, MEASURE2:23; :: thesis:

end;

now :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
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 < beta

proof

consider x being object such that
A138: x in dom g by A11, XBOOLE_0:def 1;
A139: g . x <= beta by A44, A138;
alpha <= g . x by A44, A138;
hence 0 < beta by A14, A38, A41, A42, A39, A139; :: thesis:

end;

A140: {} in S by MEASURE1:34;
A141: M . {} = 0 by VALUED_0:def 19;
dom g is Element of S by A1, Th37;
then A142: M . (dom g) <> -infty by A141, A140, MEASURE1:31, XBOOLE_1:2;
then reconsider MG = M . (dom g) as Element of REAL by A136, XXREAL_0:14;
reconsider DG = dom g as Element of S by A1, Th37;
A143: for x being object st x in dom g holds
0 <= g . x by A2;
then A144: integral' (M,g) <> -infty by A1, Th68, SUPINF_2:52;
A145: g is nonnegative by A143, SUPINF_2:52;
A146: integral' (M,g) <= beta * (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 object st x in DG holds
GP . x = beta by Th41;
A150: for x being object st x in dom (GP - g) holds
g . x <= GP . x

proof

let x be object ; :: 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 = beta by A148, A149;
hence g . x <= GP . x by A44, A148, A151; :: thesis:

end;

for x being object st x in dom GP holds
0 <= GP . x by A137, A148, A149;
then A152: GP is nonnegative by SUPINF_2:52;
then A153: dom (GP - g) = (dom GP) /\ (dom g) by A1, A145, A147, A150, Th69;
then A154: g | (dom (GP - g)) = g by A148, GRFUNC_1:23;
A155: GP | (dom (GP - g)) = GP by A148, A153, GRFUNC_1:23;
integral' (M,(g | (dom (GP - g)))) <= integral' (M,(GP | (dom (GP - g)))) by A1, A145, A147, A152, A150, Th70;
hence integral' (M,g) <= beta * (M . DG) by A137, A147, A148, A149, A154, A155, Th71; :: thesis:

end;

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

proof

let e be R_eal; :: thesis:
assume that
A158: 0 < e and
A159: e < alpha ; :: 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) in REAL by A136, A142, A165, XXREAL_0:14;
then consider y being ExtReal such that
A167: y in rng MF and
A168: (sup (rng MF)) - e < y by A158, MEASURE6:6;
consider N0 being object such that
A169: N0 in dom MF and
A170: y = MF . N0 by A167, FUNCT_1:def 3;
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:31;
then M . B0 < +infty by A136, XXREAL_0:2, XXREAL_0:4;
then A171: M . (DG \ B0) = (M . DG) - (M . B0) by A163, MEASURE1:32;
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:54;
then A172: (M . (dom g)) - (M . (H . N0)) < e by A158, A160, XXREAL_3:55;

A173: now :: thesis:

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:31, XBOOLE_1:34;
hence M . ((dom g) \ (H . n)) < e by A172, A171, XXREAL_0:2; :: thesis:

end;

now :: thesis:

reconsider XSMg = integral' (M,g) as Element of REAL by A156, A144, XXREAL_0:14;
let n be Nat; :: thesis:
A174: for x being object 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:34;
then A175: DG /\ (X \ (H . n)) in S by MEASURE1:34;
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 Element of REAL by A158, XXREAL_0:14;
A176: A misses B by XBOOLE_1:79;
beta * e = beta1 * ee by EXTREAL1:1;
then reconsider betae = beta * e as Real ;
A177: for x being object st x in dom g holds
g . x = g . x ;
A178: M . B <= M . DG by A163, MEASURE1:31;
then M . (dom g) <> -infty by A141, A140, MEASURE1:31, XBOOLE_1:2;
then A179: M . (dom g) in 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:46;
then A182: integral' (M,g) = (integral' (M,(g | A))) + (integral' (M,(g | B))) by A1, A145, Th67, XBOOLE_1:79;
M . A <= M . DG by A181, MEASURE1:31, XBOOLE_1:7;
then M . A < +infty by A136, XXREAL_0:2, XXREAL_0:4;
then beta * (M . A) < beta * +infty by A137, XXREAL_3:72;
then A183: beta * (M . A) <> +infty by A137, XXREAL_3:def 5;
A184: g | B is nonnegative by A143, Th15, SUPINF_2:52;
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:46;
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 object st x in A holds
GP . x = beta by Th41;
A190: integral' (M,GP) = beta * (M . A) by A137, A187, A188, A189, Th71;
A191: dom (g | A) = A by A181, RELAT_1:62, XBOOLE_1:7;
A192: for x being object st x in dom (GP - (g | A)) holds
(g | A) . x <= GP . x

proof

let x be object ; :: 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:61;
then x in dom g by XBOOLE_0:def 4;
then A195: g . x <= beta by A44;
(g | A) . x = g . x by A191, A188, A193, FUNCT_1:47;
hence (g | A) . x <= GP . x by A188, A189, A194, A195; :: thesis:

end;

for x being object st x in dom GP holds
0 <= GP . x by A137, A188, A189;
then A196: GP is nonnegative by SUPINF_2:52;
0 <= M . A by A141, A140, MEASURE1:31, XBOOLE_1:2;
then reconsider XSMGP = integral' (M,GP) as Element of REAL by A137, A190, A183, XXREAL_0:14;
A197: (integral' (M,g)) - (integral' (M,GP)) = XSMg - XSMGP by SUPINF_2:3;
A198: g | A is_simple_func_in S by A1, Th34;
then A199: integral' (M,(g | A)) <> -infty by A145, Th15, Th68;
A200: g | A is nonnegative by A143, Th15, SUPINF_2:52;
then A201: dom (GP - (g | A)) = (dom GP) /\ (dom (g | A)) by A198, A187, A196, A192, Th69;
then A202: GP | (dom (GP - (g | A))) = GP by A191, A188, GRFUNC_1:23;
(g | A) | (dom (GP - (g | A))) = g | A by A191, A188, A201, GRFUNC_1:23;
then A203: integral' (M,(g | A)) <= integral' (M,GP) by A198, A200, A187, A196, A192, A202, Th70;
then A204: (integral' (M,g)) - (integral' (M,GP)) <= (integral' (M,g)) - (integral' (M,(g | A))) by XXREAL_3:37;
assume N0 <= n ; :: thesis:
then M . A < e by A173;
then A205: beta * (M . A) < beta * e by A137, XXREAL_3:72;
then A206: integral' (M,(g | A)) <> +infty by A203, A190, XXREAL_0:2, XXREAL_0:4;
then reconsider XSMgA = integral' (M,(g | A)) as Element of 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:3
.= 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:15;
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 object st x in B holds
EP . x = e by A158, A160, Th41;
A214: integral' (M,EP) = e * (M . B) by A158, A211, A212, A213, Th71;
for x being object st x in dom EP holds
0 <= EP . x by A158, A212, A213;
then A215: EP is nonnegative by SUPINF_2:52;
M . B < +infty by A136, A178, XXREAL_0:2, XXREAL_0:4;
then e * (M . B) < e * +infty by A158, A160, XXREAL_3:72;
then A216: integral' (M,EP) <> +infty by A214, XXREAL_0:4;
A217: 0 <= M . B by A141, A140, MEASURE1:31, XBOOLE_1:2;
then reconsider XSMEP = integral' (M,EP) as Element of 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, Th15;
then A219: 0 <= integral' (M,((F . n) | A)) by A218, Th34, Th68;
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, Th67;
then A220: integral' (M,((F . n) | B)) <= integral' (M,(F . n)) by A219, XXREAL_3:39;
A221: M . (dom g) < +infty by A136, XXREAL_0:4;
M . B <> -infty by A141, A140, MEASURE1:31, XBOOLE_1:2;
then M . B in 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:31;
A225: g | B is_simple_func_in S by A1, Th34;
ee * MB <= ee * MG by A158, A224, XREAL_1:64;
then A226: (XSMg - betae) - (ee * MG) <= (XSMg - betae) - (ee * MB) by XREAL_1:13;
XSMEP = e * (M . B) by A158, A211, A212, A213, Th71
.= ee * MB by A222 ;
then A227: (XSMg - betae) - (ee * MB) < XSMgB - XSMEP by A210, XREAL_1:14;
betae = ee * beta1 by EXTREAL1:1;
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:61;
then A229: dom ((F . n) | B) = B by A163, A185, XBOOLE_1:28;
A230: (F . n) | B is_simple_func_in S by A3, Th34;
then A231: ((F . n) | B) + EP is_simple_func_in S by A211, Th38;
A232: (F . n) | B is nonnegative by A5, Th15;
then A233: dom (((F . n) | B) + EP) = (dom ((F . n) | B)) /\ (dom EP) by A230, A211, A215, Th65;
A234: dom (((F . n) | B) + EP) = (dom ((F . n) | B)) /\ (dom EP) by A232, A230, A211, A215, Th65
.= B by A229, A212 ;
A235: dom (g | B) = B by A180, RELAT_1:62, XBOOLE_1:7;
A236: for x being object 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 object ; :: 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:47;
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 11;
x in dom (g - (F . n)) by A240, MESFUNC1:def 11;
then A242: (g . x) - ((F . n) . x) <= e by A241, MESFUNC1:def 4;
(g | B) . x = g . x by A235, A234, A237, FUNCT_1:47;
hence (g | B) . x <= (((F . n) | B) + EP) . x by A158, A160, A239, A242, XXREAL_3:41; :: thesis:

end;

A243: ((F . n) | B) + EP is nonnegative by A232, A215, Th19;
then A244: dom ((((F . n) | B) + EP) - (g | B)) = (dom (((F . n) | B) + EP)) /\ (dom (g | B)) by A225, A184, A231, A236, Th69;
then A245: g | B = (g | B) | (dom ((((F . n) | B) + EP) - (g | B))) by A229, A212, A235, A233, GRFUNC_1:23;
((F . n) | B) + EP = (((F . n) | B) + EP) | (dom ((((F . n) | B) + EP) - (g | B))) by A229, A212, A235, A244, A233, GRFUNC_1:23;
then A246: integral' (M,(g | B)) <= integral' (M,(((F . n) | B) + EP)) by A225, A184, A231, A243, A236, A245, Th70;
integral' (M,(((F . n) | B) + EP)) = (integral' (M,(((F . n) | B) | B))) + (integral' (M,(EP | B))) by A232, A230, A211, A215, A234, Th65
.= (integral' (M,(((F . n) | B) | B))) + (integral' (M,EP)) by A212, GRFUNC_1:23
.= (integral' (M,((F . n) | B))) + (integral' (M,EP)) by FUNCT_1:51 ;
then A247: (integral' (M,(g | B))) - (integral' (M,EP)) <= integral' (M,((F . n) | B)) by A158, A214, A217, A216, A246, XXREAL_3:42;
beta1 + MG = beta + (M . (dom g)) by A223;
then ee * (beta1 + MG) = e * (beta + (M . (dom g))) ;
then A248: XSMg - (ee * (beta1 + MG)) = (integral' (M,g)) - (e * (beta + (M . (dom g)))) ;
(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,((F . n) | B)) by A247, A228, A248, XXREAL_0:2;
hence (integral' (M,g)) - (e * (beta + (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 * (beta + (M . (dom g)))) < integral' (M,(F . n)) ; :: thesis:

end;

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

proof

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

now :: thesis:

let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then (integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n)) by A252;
hence (integral' (M,g)) - (e * (beta + (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 * (beta + (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 < alpha & e * (beta + (M . (dom g))) <= e1 )

proof

reconsider ralpha = alpha as Real ;
reconsider rdomg = M . (dom g) as Element of REAL by A136, A142, XXREAL_0:14;
let e1 be R_eal; :: thesis:
assume A254: 0 < e1 ; :: thesis:
{} c= DG ;
then A255: 0 <= rdomg by A141, A140, MEASURE1:31;

per cases ;

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

reconsider z = ralpha / 2 as R_eal by XXREAL_0:def 1;
z * (beta + (M . (dom g))) <= +infty by XXREAL_0:4;
hence ex e being R_eal st
( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 ) by A43, A256, XREAL_1:216; :: thesis:

end;

suppose e1 <> +infty ; :: thesis:

then reconsider re1 = e1 as Element of 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:216;
then A258: min ((re1 / (beta1 + rdomg)),(ralpha / 2)) < ralpha by A257, XXREAL_0:2;
beta1 + rdomg = beta1 + rdomg ;
then A259: (min ((re1 / (beta1 + rdomg)),(ralpha / 2))) * (beta1 + rdomg) = (min ((re1 / (beta1 + rdomg)),(ralpha / 2))) * (beta + (M . (dom g))) ;
A260: (min ((re1 / (beta1 + rdomg)),(ralpha / 2))) * (beta1 + rdomg) <= (re1 / (beta1 + rdomg)) * (beta1 + rdomg) by A137, A255, XREAL_1:64, XXREAL_0:17;
reconsider z = min ((re1 / (beta1 + rdomg)),(ralpha / 2)) as R_eal by XXREAL_0:def 1;
take z ; :: thesis:

A261: now :: thesis:

per cases by XXREAL_0:15;

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

hence 0 < z by A137, A254, A255; :: thesis:

end;

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

hence 0 < z by A43; :: thesis:

end;

z * (beta1 + rdomg) <= re1 by A137, A255, XCMPLX_1:87, A260;
hence ( 0 < z & z < alpha & z * (beta + (M . (dom g))) <= e1 ) by A261, A258, A259; :: thesis:

end;

A262: 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
A263: 0 < e and
A264: e < alpha and
A265: e * (beta + (M . (dom g))) <= e1 by A253;
consider N0 being Nat such that
A266: for n being Nat st N0 <= n holds
(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n by A249, A263, A264;
take N0 ; :: thesis:

now :: thesis:

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

end;

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

end;

A268: 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, Th68;
hence 0 <= L . n by A8; :: thesis:

end;

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

proof

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

proof

let x be object ; :: 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, A273, A270, A272; :: thesis:

end;

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

end;

per cases ;

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

then consider K being Real such that
0 < K and
A281: for n being Nat holds L . n < K ;

now :: thesis:

let x be ExtReal; :: thesis:
assume x in rng L ; :: thesis:
then ex z being object st
( z in dom L & x = L . z ) by FUNCT_1:def 3;
hence x <= K by A281; :: thesis:

end;

then K is UpperBound of rng L by XXREAL_2:def 1;
then A282: sup (rng L) <= K by XXREAL_2:def 3;
K in REAL by XREAL_0:def 1;
then A283: sup (rng L) <> +infty by A282, XXREAL_0:9;
A284: 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 12;
dom L = NAT by FUNCT_2:def 1;
then A285: L . n in rng L by FUNCT_1:def 3;
sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;
hence L . n <= sup (rng L) by A285, XXREAL_2:def 1; :: thesis:

end;

then L . 1 <= sup (rng L) ;
then A286: sup (rng L) <> -infty by A268;
then reconsider h = sup (rng L) as Element of REAL by A283, XXREAL_0:14;
A287: for p being Real 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; :: thesis:
assume A288: 0 < p ; :: thesis:
A289: sup (rng L) <> (sup (rng L)) + p

proof

assume A290: sup (rng L) = (sup (rng L)) + p ; :: thesis:
(p + (sup (rng L))) + (- (sup (rng L))) = p + ((sup (rng L)) + (- (sup (rng L)))) by A286, A283, XXREAL_3:29
.= p + 0 by XXREAL_3:7
.= p ;
hence contradiction by A288, A290, XXREAL_3:7; :: thesis:

end;

sup (rng L) in REAL by A286, A283, XXREAL_0:14;
then consider y being ExtReal such that
A291: y in rng L and
A292: (sup (rng L)) - p < y by A288, MEASURE6:6;
consider x being object such that
A293: x in dom L and
A294: y = L . x by A291, FUNCT_1:def 3;
reconsider N0 = x as Element of NAT by A293;
take N0 ; :: thesis:
let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then L . N0 <= L . n by A269;
then (sup (rng L)) - p < L . n by A292, A294, XXREAL_0:2;
then sup (rng L) < (L . n) + p by XXREAL_3:54;
then (sup (rng L)) - (L . n) < p by XXREAL_3:55;
then - p < - ((sup (rng L)) - (L . n)) by XXREAL_3:38;
then A295: - p < (L . n) - (sup (rng L)) by XXREAL_3:26;
A296: L . n <= sup (rng L) by A284;
(sup (rng L)) + 0. <= (sup (rng L)) + p by A288, XXREAL_3:36;
then sup (rng L) <= (sup (rng L)) + p by XXREAL_3:4;
then sup (rng L) < (sup (rng L)) + p by A289, XXREAL_0:1;
then L . n < (sup (rng L)) + p by A296, XXREAL_0:2;
then (L . n) - (sup (rng L)) < p by XXREAL_3:55;
hence |.((L . n) - (sup (rng L))).| < p by A295, EXTREAL1:22; :: thesis:

end;

A297: h = sup (rng L) ;
then A298: L is convergent_to_finite_number by A287;
hence L is convergent ; :: thesis:
then A299: lim L = sup (rng L) by A287, A297, A298, Def12;

now :: thesis:

let e be Real; :: thesis:
assume A300: 0 < e ; :: thesis:
reconsider ee = e as R_eal by XXREAL_0:def 1;
consider N0 being Nat such that
A301: for n being Nat st N0 <= n holds
(integral' (M,g)) - ee < L . n by A262, A300;
A302: L . N0 <= sup (rng L) by A284;
(integral' (M,g)) - ee < L . N0 by A301;
then (integral' (M,g)) - ee < sup (rng L) by A302, XXREAL_0:2;
hence integral' (M,g) < (lim L) + e by A299, XXREAL_3:54; :: thesis:

end;

hence integral' (M,g) <= lim L by XXREAL_3:61; :: thesis:

end;

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

now :: thesis:

let K be Real; :: thesis:
assume 0 < K ; :: thesis:
then consider N0 being Nat such that
A304: K <= L . N0 by A303;

now :: thesis:

let n be Nat; :: thesis:
assume N0 <= n ; :: thesis:
then L . N0 <= L . n by A269;
hence K <= L . n by A304, 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 A305: L is convergent_to_+infty ;
hence L is convergent ; :: thesis:
then lim L = +infty by A305, Def12;
hence integral' (M,g) <= lim L by XXREAL_0:4; :: thesis:

end;

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

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

proof

let e be R_eal; :: thesis:
assume that
A308: 0 < e and
A309: e < alpha ; :: thesis:
A310: 0 <= alpha - e by A309, XXREAL_3:40;
consider H being SetSequence of X, MF being ExtREAL_sequence such that
A311: 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
A312: 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
A313: for n being Nat holds H . n in S by A61, A308, A309;
A314: e <> +infty by A309, XXREAL_0:4;

now :: thesis:

let n be Nat; :: thesis:
reconsider B = H . n as Element of S by A313;
A315: for x being object st x in dom (F . n) holds
(F . n) . x = (F . n) . x ;
H . n in S by A313;
then A316: X \ (H . n) in S by MEASURE1:34;
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 A316, MEASURE1:34;
A317: dom (F . n) = dom g by A4;
A318: DG = DG \/ (H . n) by A312, XBOOLE_1:12
.= (DG \ (H . n)) \/ (H . n) by XBOOLE_1:39 ;
then dom (F . n) = (A \/ B) /\ (dom (F . n)) by A317;
then A319: F . n = (F . n) | (A \/ B) by A315, FUNCT_1:46;
consider EP being PartFunc of X,ExtREAL such that
A320: EP is_simple_func_in S and
A321: dom EP = B and
A322: for x being object st x in B holds
EP . x = alpha - e by A308, A310, Th41, XXREAL_3:18;
for x being object st x in dom EP holds
0 <= EP . x by A310, A321, A322;
then A323: EP is nonnegative by SUPINF_2:52;
A324: dom ((F . n) | B) = (dom (F . n)) /\ B by RELAT_1:61
.= B by A318, A317, XBOOLE_1:7, XBOOLE_1:28 ;
A325: for x being object st x in dom (((F . n) | B) - EP) holds
EP . x <= ((F . n) | B) . x

proof

set f = g - (F . n);
let x be object ; :: 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 A326: x in (dom ((F . n) | B)) /\ (dom EP) by XBOOLE_0:def 5;
then A327: x in dom ((F . n) | B) by XBOOLE_0:def 4;
then A328: ((F . n) | B) . x = (F . n) . x by FUNCT_1:47;
A329: x in less_dom ((g - (F . n)),e) by A311, A324, A327;
then A330: x in dom (g - (F . n)) by MESFUNC1:def 11;
(g - (F . n)) . x < e by A329, MESFUNC1:def 11;
then (g . x) - ((F . n) . x) <= e by A330, MESFUNC1:def 4;
then g . x <= ((F . n) . x) + e by A308, A314, XXREAL_3:41;
then A331: (g . x) - e <= (F . n) . x by A308, A314, XXREAL_3:42;
dom (g - (F . n)) = dom g by A56;
then alpha <= g . x by A44, A330;
then alpha - e <= (g . x) - e by XXREAL_3:37;
then alpha - e <= (F . n) . x by A331, XXREAL_0:2;
hence EP . x <= ((F . n) | B) . x by A324, A321, A322, A326, A328; :: thesis:

end;

A332: F . n is_simple_func_in S by A3;
(F . n) | A is nonnegative by A5, Th15;
then A333: 0 <= integral' (M,((F . n) | A)) by A332, Th34, Th68;
A334: 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, A319, A334, Th67;
then A335: integral' (M,((F . n) | B)) <= integral' (M,(F . n)) by A333, XXREAL_3:39;
A336: (F . n) | B is_simple_func_in S by A3, Th34;
A337: (F . n) | B is nonnegative by A5, Th15;
then A338: dom (((F . n) | B) - EP) = (dom ((F . n) | B)) /\ (dom EP) by A336, A320, A323, A325, Th69;
then A339: EP | (dom (((F . n) | B) - EP)) = EP by A324, A321, GRFUNC_1:23;
A340: ((F . n) | B) | (dom (((F . n) | B) - EP)) = (F . n) | B by A324, A321, A338, GRFUNC_1:23;
integral' (M,(EP | (dom (((F . n) | B) - EP)))) <= integral' (M,(((F . n) | B) | (dom (((F . n) | B) - EP)))) by A337, A336, A320, A323, A325, Th70;
then A341: integral' (M,EP) <= integral' (M,(F . n)) by A335, A339, A340, XXREAL_0:2;
integral' (M,EP) = (alpha - e) * (M . B) by A309, A320, A321, A322, Th71, XXREAL_3:40;
hence (alpha - e) * (M . (less_dom ((g - (F . n)),e))) <= integral' (M,(F . n)) by A311, A341; :: thesis:

end;

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

end;

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

proof

reconsider ralpha = alpha as Real ;
reconsider e = alpha / 2 as R_eal by XXREAL_0:def 1;
let y be Real; :: thesis:
assume 0 < y ; :: thesis:
set a2 = ralpha / 2;
reconsider y1 = y as Real ;
y = (ralpha - (ralpha / 2)) * (y1 / (ralpha - (ralpha / 2))) by A43, XCMPLX_1:87;
then A342: y = (ralpha - (ralpha / 2)) * (y1 / (ralpha - (ralpha / 2))) ;
A343: e = ralpha / 2 ;
then consider H being SetSequence of X, MF being ExtREAL_sequence such that
A344: for n being Nat holds H . n = less_dom ((g - (F . n)),e) and
A345: 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
A346: for n being Nat holds MF . n = M . (H . n) and
A347: M . (dom g) = sup (rng MF) and
A348: for n being Nat holds H . n in S by A61, A43, XREAL_1:216;
A349: y / (ralpha - (ralpha / 2)) in REAL by XREAL_0:def 1;
A350: y / (alpha - e) < +infty by XXREAL_0:9, A349;
ex z being ExtReal st
( z in rng MF & y / (alpha - e) <= z )

proof

assume for z being ExtReal holds
( not z in rng MF or not y / (alpha - e) <= z ) ; :: thesis:
then for z being ExtReal st z in rng MF holds
z <= y / (alpha - e) ;
then y / (alpha - e) is UpperBound of rng MF by XXREAL_2:def 1;
hence contradiction by A306, A350, A347, XXREAL_2:def 3; :: thesis:

end;

then consider z being R_eal such that
A351: z in rng MF and
A352: y / (alpha - e) <= z ;
(ralpha / 2) - (ralpha / 2) < ralpha - (ralpha / 2) by A43;
then A353: 0 < alpha - e ;
consider x being object such that
A354: x in dom MF and
A355: z = MF . x by A351, FUNCT_1:def 3;
reconsider N0 = x as Element of NAT by A354;
take N0 ; :: thesis:
A356: (alpha - e) * (y / (alpha - e)) = y by A342;
thus for m being Nat st N0 <= m holds
y <= L . m :: thesis:

proof

y / (alpha - e) <= M . (H . N0) by A346, A352, A355;
then A357: y <= (alpha - e) * (M . (H . N0)) by A353, A356, XXREAL_3:71;
let m be Nat; :: thesis:
A358: H . m in S by A348;
assume N0 <= m ; :: thesis:
then A359: H . N0 c= H . m by A345;
H . N0 in S by A348;
then (alpha - e) * (M . (H . N0)) <= (alpha - e) * (M . (H . m)) by A353, A359, A358, MEASURE1:31, XXREAL_3:71;
then y <= (alpha - e) * (M . (H . m)) by A357, XXREAL_0:2;
then A360: y <= (alpha - e) * (M . (less_dom ((g - (F . m)),e))) by A344;
(alpha - e) * (M . (less_dom ((g - (F . m)),e))) <= integral' (M,(F . m)) by A43, A307, A343, XREAL_1:216;
then y <= integral' (M,(F . m)) by A360, XXREAL_0:2;
hence y <= L . m by A8; :: thesis:

end;

then A361: L is convergent_to_+infty ;
hence L is convergent ; :: thesis:
then ( ex g being Real st
( lim L = g & ( for p being Real 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 A361, Th50, XXREAL_0:4; :: thesis:

end;