let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for g being PartFunc of X,ExtREAL
for F being Functional_Sequence of X,ExtREAL
for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' M,(F . n) ) holds
( L is convergent & integral' M,g <= lim L )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for g being PartFunc of X,ExtREAL
for F being Functional_Sequence of X,ExtREAL
for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' M,(F . n) ) holds
( L is convergent & integral' M,g <= lim L )
let M be sigma_Measure of S; :: thesis: for g being PartFunc of X,ExtREAL
for F being Functional_Sequence of X,ExtREAL
for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' M,(F . n) ) holds
( L is convergent & integral' M,g <= lim L )
let g be PartFunc of X,ExtREAL ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' M,(F . n) ) holds
( L is convergent & integral' M,g <= lim L )
let F be Functional_Sequence of X,ExtREAL ; :: thesis: for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' M,(F . n) ) holds
( L is convergent & integral' M,g <= lim L )
let L be ExtREAL_sequence; :: thesis: ( g is_simple_func_in S & ( for x being set st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' M,(F . n) ) implies ( L is convergent & integral' M,g <= lim L ) )
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: ( L is convergent & integral' M,g <= lim L )

per cases ( dom g = {} or dom g <> {} ) ;

suppose A9: dom g = {} ; :: thesis: ( L is convergent & integral' M,g <= lim L )

now

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

end;

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

end;

suppose A11: dom g <> {} ; :: thesis: ( L is convergent & integral' M,g <= lim L )

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 & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds
( 0 < a . n & a . n < +infty ) ) ) by A1, MESFUNC3:14;
A13: len a <> 0

proof

assume len a = 0 ; :: thesis: contradiction
then A14: dom a = Seg 0 by FINSEQ_1:def 3;
A15: rng G = {}

proof

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

end;

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

end;

defpred S₁[ Nat, set ] means $2 = a . $1;
A18: 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: ( k in Seg (len a) implies ex x being Element of REAL st S₁[k,x] )
assume k in Seg (len a) ; :: thesis: ex x being Element of REAL st S₁[k,x]
then A19: ( 1 <= k & k <= len a & k in dom a ) by FINSEQ_1:3, FINSEQ_1:def 3;

per cases ( k = 1 or k <> 1 ) ;

suppose A20: k = 1 ; :: thesis: ex x being Element of REAL st S₁[k,x]

take x = 0 ; :: thesis: S₁[k,x]
thus S₁[k,x] by A12, A20; :: thesis: verum

end;

suppose k <> 1 ; :: thesis: ex x being Element of REAL st S₁[k,x]

then k > 1 by A19, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then ( 0 < a . k & a . k < +infty ) by A12, A19;
then reconsider x = a . k as Element of REAL by XXREAL_0:14;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] ; :: thesis: verum

end;

end;

end;

consider a1 being FinSequence of REAL such that
A21: ( 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(A18);
A22: 2 <= len a

proof

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

end;

then A27: 2 in dom a1 by A21;
then ( a1 . 2 = a . 2 & 2 in dom a ) by A21, FINSEQ_1:def 3;
then A28: a1 . 2 <> a . 1 by A12;
1 <= len a by A22, XXREAL_0:2;
then 1 in Seg (len a) ;
then a . 1 = a1 . 1 by A21;
then ( not a1 . 2 in {(a1 . 1)} & a1 . 2 in rng a1 ) by A27, A28, FUNCT_1:12, TARSKI:def 1;
then reconsider RINGA = (rng a1) \ {(a1 . 1)} as non empty finite real-membered set by XBOOLE_0:def 5;
set alpha = R_EAL (min RINGA);
set beta = R_EAL (max RINGA);
reconsider beta1 = max RINGA as Real by XREAL_0:def 1;
min RINGA in RINGA by XXREAL_2:def 7;
then A29: ( min RINGA in rng a1 & not min RINGA in {(a1 . 1)} ) by XBOOLE_0:def 5;
then consider i being set such that
A30: ( i in dom a1 & min RINGA = a1 . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A30;
A31: i <> 1 by A29, A30, TARSKI:def 1;
i in Seg (len a1) by A30, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:3;
then 1 < i by A31, XXREAL_0:1;
then A32: 1 + 1 <= i by NAT_1:13;
A33: g is real-valued by A1, MESFUNC2:def 5;
A34: for n being Nat holds dom (g - (F . n)) = dom g

proof

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

end;

A37: 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: ( R_EAL 0 < e & e < R_EAL (min RINGA) implies 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 ) ) )
assume A38: ( R_EAL 0 < e & e < R_EAL (min RINGA) ) ; :: thesis: 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 ) )
deffunc H₁( Nat) -> Element of bool X = less_dom (g - (F . $1)),e;
consider H being SetSequence of X such that
A39: for n being Element of NAT holds H . n = H₁(n) from FUNCT_2:sch 4();

A40: now

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

end;

A41: for n, m being Nat st n <= m holds
H . n c= H . m

proof

let n, m be Nat; :: thesis: ( n <= m implies H . n c= H . m )
assume A42: n <= m ; :: thesis: H . n c= H . m

now

let x be set ; :: thesis: ( x in H . n implies x in H . m )
assume x in H . n ; :: thesis: x in H . m
then A43: x in less_dom (g - (F . n)),e by A40;
then A44: ( x in dom (g - (F . n)) & (g - (F . n)) . x < e ) by MESFUNC1:def 12;
then A45: (g - (F . n)) . x = (g . x) - ((F . n) . x) by MESFUNC1:def 4;
A46: (g - (F . n)) . x < e by A43, MESFUNC1:def 12;
A47: ( dom (g - (F . n)) = dom g & dom (g - (F . m)) = dom g ) by A34;
then A48: (g - (F . m)) . x = (g . x) - ((F . m) . x) by A44, MESFUNC1:def 4;
A49: (F . n) . x <= (F . m) . x by A6, A42, A44, A47;
(g - (F . m)) . x <= (g - (F . n)) . x by A45, A48, A49, XXREAL_3:39;
then (g - (F . m)) . x < e by A46, XXREAL_0:2;
then x in less_dom (g - (F . m)),e by A44, A47, MESFUNC1:def 12;
hence x in H . m by A40; :: thesis: verum

end;

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

end;

now

let x be set ; :: thesis: ( x in lim_inf H implies x in dom g )
assume x in lim_inf H ; :: thesis: x in dom g
then x in Union (inferior_setsequence H) by SETLIM_1:def 4;
then consider V being set such that
A50: ( x in V & V in rng (inferior_setsequence H) ) by TARSKI:def 4;
consider n being set such that
A51: ( n in dom (inferior_setsequence H) & V = (inferior_setsequence H) . n ) by A50, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A51;
x in H . (n + 0 ) by A50, A51, SETLIM_1:19;
then x in less_dom (g - (F . n)),e by A40;
then x in dom (g - (F . n)) by MESFUNC1:def 12;
hence x in dom g by A34; :: thesis: verum

end;

then A52: lim_inf H c= dom g by TARSKI:def 3;
dom g c= lim_inf H

proof

now

let x be set ; :: thesis: ( x in dom g implies x in lim_inf H )
assume A53: x in dom g ; :: thesis: x in lim_inf H
then reconsider x1 = x as Element of X ;
A54: ( F # x1 is convergent & g . x <= lim (F # x1) ) by A7, A53;

A55: now

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

end;

now

per cases ( F # x1 is convergent_to_finite_number or F # x1 is convergent_to_+infty ) by A54, A55, Def11;

suppose A59: F # x1 is convergent_to_finite_number ; :: thesis: ex N being Nat st
( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N )

( 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 A54, Def12;
then consider limFx being real number such that
A60: ( 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 ) ) by A59, Th56, Th57;
reconsider E = e as Real by A38, XXREAL_0:48;
g . x <= lim (F # x1) by A7, A53;
then (g . x) - (R_EAL (E / 2)) <= (lim (F # x1)) - 0. by A38, XXREAL_3:39;
then A62: (g . x) - (R_EAL (E / 2)) <= lim (F # x1) by XXREAL_3:4;
consider N being Nat such that
A63: for m being Nat st N <= m holds
|.(((F # x1) . m) - (lim (F # x1))).| < R_EAL (E / 2) by A60, A38;
reconsider N = N as Element of NAT by ORDINAL1:def 13;

now

let k be Element of NAT ; :: thesis: x in H . (N + k)
set m = N + k;
A76: x1 in dom (g - (F . (N + k))) by A34, A53;
A77: g . x <= (lim (F # x1)) + (R_EAL (E / 2)) by A62, XXREAL_3:44;
|.(((F # x1) . (N + k)) - (lim (F # x1))).| < R_EAL (E / 2) by A63, NAT_1:11;
then ( (F # x1) . (N + k) <> +infty & (F # x1) . (N + k) <> -infty ) by A60, Th3;
then A74: ( (F . (N + k)) . x <> +infty & (F . (N + k)) . x <> -infty ) by Def13;

B68: now

let e be real number ; :: thesis: ( 0 < e implies (F # x1) . (N + k) < (lim (F # x1)) + e )
assume 0 < e ; :: thesis: (F # x1) . (N + k) < (lim (F # x1)) + e
then consider N0 being Nat such that
A65: for M being Nat st N0 <= M holds
|.(((F # x1) . M) - (lim (F # x1))).| < R_EAL e by A60;
reconsider N0 = N0, n1 = N + k as Element of NAT by ORDINAL1:def 13;
set M = max N0,n1;
A66: |.(((F # x1) . (max N0,n1)) - (lim (F # x1))).| < R_EAL e by A65, XXREAL_0:25;
((F # x1) . (max N0,n1)) - (lim (F # x1)) <= |.(((F # x1) . (max N0,n1)) - (lim (F # x1))).| by EXTREAL2:57;
then ((F # x1) . (max N0,n1)) - (lim (F # x1)) < R_EAL e by A66, XXREAL_0:2;
then A67: (F # x1) . (max N0,n1) < (R_EAL e) + (lim (F # x1)) by A60, XXREAL_3:65;
(F . (N + k)) . x1 <= (F . (max N0,n1)) . x1 by A6, A53, XXREAL_0:25;
then (F . (N + k)) . x1 <= (F # x1) . (max N0,n1) by Def13;
then (F # x1) . (N + k) <= (F # x1) . (max N0,n1) by Def13;
hence (F # x1) . (N + k) < (lim (F # x1)) + e by A67, XXREAL_0:2; :: thesis: verum

end;

(F # x1) . (N + k) <= lim (F # x1) by B68, XXREAL_3:72;
then A71: 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 A71, EXTREAL1:def 3 ;
then (lim (F # x1)) - ((F # x1) . (N + k)) < R_EAL (E / 2) by A63, NAT_1:11;
then (lim (F # x1)) - ((F . (N + k)) . x1) < R_EAL (E / 2) by Def13;
then lim (F # x1) < ((F . (N + k)) . x) + (R_EAL (E / 2)) by A74, XXREAL_3:65;
then (lim (F # x1)) + (E / 2) < (((F . (N + k)) . x) + (R_EAL (E / 2))) + (E / 2) by XXREAL_3:73;
then g . x < (((F . (N + k)) . x1) + (R_EAL (E / 2))) + (R_EAL (E / 2)) by A77, 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 A76, MESFUNC1:def 4;
then x in less_dom (g - (F . (N + k))),e by A76, MESFUNC1:def 12;
hence x in H . (N + k) by A40; :: thesis: verum

end;

then A79: 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 A79; :: thesis: verum

end;

suppose A80: F # x1 is convergent_to_+infty ; :: thesis: ex N being Nat st
( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N )

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

proof

B81: e in REAL by A38, XXREAL_0:48;

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

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

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

now

let m be Nat; :: thesis: ( N <= m implies (g . x1) - ((F . m) . x1) < e )
assume N <= m ; :: thesis: (g . x1) - ((F . m) . x1) < e
then (g . x1) - e < (F # x1) . m by A82, A83;
then g . x1 < ((F # x1) . m) + e by B81, XXREAL_3:65;
then (g . x1) - ((F # x1) . m) < e by B81, XXREAL_3:66;
hence (g . x1) - ((F . m) . x1) < e by Def13; :: thesis: verum

end;

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

end;

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

reconsider gx1 = g . x as Real by A33, XXREAL_0:14;
reconsider e1 = e as Real by A38, XXREAL_0:48;
(g . x) - e = gx1 - e1 by SUPINF_2:5;
then reconsider ee = (g . x1) - e as Real ;
A86: R_EAL ee < R_EAL (ee + 1) by XREAL_1:31;
consider N being Nat such that
A87: for m being Nat st N <= m holds
R_EAL (ee + 1) <= (F # x1) . m by A80, A84, Def9;

now

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

end;

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

end;

end;

end;

then consider N being Nat such that
A88: 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;

A89: now

let m be Nat; :: thesis: ( N <= m implies x1 in less_dom (g - (F . m)),e )
assume N <= m ; :: thesis: x1 in less_dom (g - (F . m)),e
then A90: (g . x1) - ((F . m) . x1) < e by A88;
x1 in dom (g - (F . m)) by A34, A53;
then ( x1 in dom (g - (F . m)) & (g - (F . m)) . x1 < e ) by A90, MESFUNC1:def 4;
hence x1 in less_dom (g - (F . m)),e by MESFUNC1:def 12; :: thesis: verum

end;

now

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

end;

then A91: 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 A91; :: thesis: verum

end;

end;

end;

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

end;

hence dom g c= lim_inf H by TARSKI:def 3; :: thesis: verum

end;

then A93: lim_inf H = dom g by A52, XBOOLE_0:def 10;
A94: for n being Nat holds H . n c= dom g

proof

let n be Nat; :: thesis: H . n c= dom g

now

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

end;

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

end;

for n, m being Element of NAT st n <= m holds
H . n c= H . m by A41;
then A95: H is non-descending by PROB_1:def 7;
A96: Union H c= dom g

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union H or x in dom g )
assume x in Union H ; :: thesis: x in dom g
then consider n being Element of NAT such that
A97: x in H . n by PROB_1:25;
H . n c= dom g by A94;
hence x in dom g by A97; :: thesis: verum

end;

A98: lim_inf H c= lim_sup H by KURATO_2:9;
deffunc H₂( Nat) -> Element of ExtREAL = M . (H . $1);
consider MF being ExtREAL_sequence such that
A99: for n being Element of NAT holds MF . n = H₂(n) from FUNCT_2:sch 4();

A100: now

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

end;

A101: ( M . (dom g) = sup (rng MF) & ( for n being Element of NAT holds H . n in S ) )

proof

A102: now

let x be set ; :: thesis: ( x in NAT implies H . x in S )
assume x in NAT ; :: thesis: H . x in S
then reconsider n = x as Element of NAT ;
A103: F . n is_simple_func_in S by A3;
then consider GF being Finite_Sep_Sequence of S such that
A104: ( dom (F . n) = union (rng GF) & ( 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;
reconsider DGH = union (rng GF) as Element of S by MESFUNC2:34;
A105: ( g is real-valued & F . n is real-valued ) by A1, A103, MESFUNC2:def 5;
A106: g is_measurable_on DGH by A1, MESFUNC2:37;
reconsider E = e as Real by A38, XXREAL_0:48;
F . n is_measurable_on DGH by A3, MESFUNC2:37;
then g - (F . n) is_measurable_on DGH by A104, A105, A106, MESFUNC2:13;
then A107: DGH /\ (less_dom (g - (F . n)),(R_EAL E)) in S by MESFUNC1:def 17;
A108: less_dom (g - (F . n)),(R_EAL E) c= dom (g - (F . n))

proof

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

end;

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 A34, A104;
then DGH /\ (less_dom (g - (F . n)),(R_EAL E)) = less_dom (g - (F . n)),(R_EAL E) by A108, XBOOLE_1:28;
hence H . x in S by A40, A107; :: thesis: verum

end;

dom H = NAT by FUNCT_2:def 1;
then reconsider HH = H as Function of NAT ,S by A102, FUNCT_2:5;
A109: for n being Element of NAT holds HH . n c= HH . (n + 1) by A41, NAT_1:11;
lim_sup H = Union H by A95, SETLIM_1:59;
then A110: M . (union (rng H)) = M . (dom g) by A93, A96, A98, XBOOLE_0:def 10;
A111: ( dom MF = NAT & dom H = NAT ) by FUNCT_2:def 1;
rng HH c= S by RELAT_1:def 19;
then A112: rng H c= dom M by FUNCT_2:def 1;
A113: 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: ( x in dom MF iff ( x in dom H & H . x in dom M ) )

now

assume A114: x in dom MF ; :: thesis: ( x in dom H & H . x in dom M )
then H . x in rng H by A111, FUNCT_1:12;
hence ( x in dom H & H . x in dom M ) by A111, A112, A114; :: thesis: verum

end;

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

end;

for x being set st x in dom MF holds
MF . x = M . (H . x) by A99;
then M * H = MF by A113, FUNCT_1:20;
hence ( M . (dom g) = sup (rng MF) & ( for n being Element of NAT holds H . n in S ) ) by A102, A109, A110, MEASURE2:27; :: thesis: verum

end;

now

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

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 A40, A41, A94, A100, A101; :: thesis: verum

end;

A115: ( i in dom a & a . i = R_EAL (a1 . i) ) by A21, A30, FINSEQ_1:def 3;
then A116: 0 < R_EAL (min RINGA) by A12, A30, A32;
A117: 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: ( x in dom g implies ( R_EAL (min RINGA) <= g . x & g . x <= R_EAL (max RINGA) ) )
assume A118: x in dom g ; :: thesis: ( R_EAL (min RINGA) <= g . x & g . x <= R_EAL (max RINGA) )
then x in union (rng G) by A12, MESFUNC3:def 1;
then consider Y being set such that
A119: ( x in Y & Y in rng G ) by TARSKI:def 4;
consider k being set such that
A120: ( k in dom G & Y = G . k ) by A119, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A120;
k in dom a by A12, A120, MESFUNC3:def 1;
then A121: k in Seg (len a) by FINSEQ_1:def 3;
then A122: a1 . k in rng a1 by A21, FUNCT_1:12;

now

assume A123: a1 . k = a1 . 1 ; :: thesis: contradiction
1 <= len a by A22, XXREAL_0:2;
then A124: 1 in dom a1 by A21;
a . k = a1 . k by A21, A121;
then A125: a . k = a . 1 by A21, A123, A124;
g . x = a . k by A12, A119, A120, MESFUNC3:def 1;
hence contradiction by A2, A12, A118, A125; :: thesis: verum

end;

then not a1 . k in {(a1 . 1)} by TARSKI:def 1;
then A126: a1 . k in RINGA by A122, XBOOLE_0:def 5;
g . x = a . k by A12, A119, A120, MESFUNC3:def 1
.= a1 . k by A21, A121 ;
hence ( R_EAL (min RINGA) <= g . x & g . x <= R_EAL (max RINGA) ) by A126, XXREAL_2:def 7, XXREAL_2:def 8; :: thesis: verum

end;

per cases ( M . (dom g) <> +infty or M . (dom g) = +infty ) ;

suppose A127: M . (dom g) <> +infty ; :: thesis: ( L is convergent & integral' M,g <= lim L )

reconsider DG = dom g as Element of S by A1, Th43;
A128: M . {} = 0 by VALUED_0:def 19;
A129: {} in S by MEASURE1:66;
( {} c= dom g & dom g is Element of S ) by A1, Th43, XBOOLE_1:2;
then A130: ( M . (dom g) <> -infty & M . (dom g) <> +infty ) by A127, A128, A129, MEASURE1:62;
B131: for x being set st x in dom g holds
0 <= g . x by A2;
then A131: g is nonnegative by SUPINF_2:71;
A132: 0 < R_EAL (max RINGA)

proof

consider x being set such that
A133: x in dom g by A11, XBOOLE_0:def 1;
( R_EAL (min RINGA) <= g . x & g . x <= R_EAL (max RINGA) ) by A117, A133;
hence 0 < R_EAL (max RINGA) by A12, A30, A32, A115; :: thesis: verum

end;

A134: integral' M,g <= (R_EAL (max RINGA)) * (M . DG)

proof

consider GP being PartFunc of X,ExtREAL such that
A135: ( GP is_simple_func_in S & dom GP = DG & ( for x being set st x in DG holds
GP . x = R_EAL (max RINGA) ) ) by Th47;
for x being set st x in dom GP holds
0 <= GP . x by A132, A135;
then A136: GP is nonnegative by SUPINF_2:71;
A137: for x being set st x in dom (GP - g) holds
g . x <= GP . x

proof

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

end;

then A139: integral' M,(g | (dom (GP - g))) <= integral' M,(GP | (dom (GP - g))) by A1, A131, A135, A136, Th76;
dom (GP - g) = (dom GP) /\ (dom g) by A1, A131, A135, A136, A137, Th75;
then ( g | (dom (GP - g)) = g & GP | (dom (GP - g)) = GP ) by A135, GRFUNC_1:64;
hence integral' M,g <= (R_EAL (max RINGA)) * (M . DG) by A132, A135, A139, Th77; :: thesis: verum

end;

reconsider MG = M . (dom g) as Real by A130, XXREAL_0:14;
(R_EAL (max RINGA)) * (M . DG) = beta1 * MG by EXTREAL1:13;
then A140: ( integral' M,g <> +infty & integral' M,g <> -infty ) by A1, B131, A134, Th74, SUPINF_2:71, XXREAL_0:9;
A141: 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: ( 0 < e & e < R_EAL (min RINGA) implies 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) )
assume A142: ( 0 < e & e < R_EAL (min RINGA) ) ; :: thesis: 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)
then A143: ( e <> -infty & e <> +infty ) by XXREAL_0:4;
consider H being SetSequence of X, MF being ExtREAL_sequence such that
A144: for n being Nat holds H . n = less_dom (g - (F . n)),e and
A145: for n, m being Nat st n <= m holds
H . n c= H . m and
A146: for n being Nat holds H . n c= dom g and
A147: for n being Nat holds MF . n = M . (H . n) and
A148: M . (dom g) = sup (rng MF) and
A149: for n being Nat holds H . n in S by A37, A142;
sup (rng MF) is Real by A130, A148, XXREAL_0:14;
then consider y being ext-real number such that
A150: ( y in rng MF & (sup (rng MF)) - e < y ) by A142, MEASURE6:33;
consider N0 being set such that
A151: ( N0 in dom MF & y = MF . N0 ) by A150, FUNCT_1:def 5;
reconsider N0 = N0 as Element of NAT by A151;
reconsider B0 = H . N0 as Element of S by A149;
(M . (dom g)) - e < M . (H . N0) by A147, A148, A150, A151;
then M . (dom g) < (M . (H . N0)) + e by A143, XXREAL_3:65;
then A152: (M . (dom g)) - (M . (H . N0)) < e by A143, XXREAL_3:66;
M . B0 <= M . DG by A146, MEASURE1:62;
then M . B0 < +infty by A127, XXREAL_0:2, XXREAL_0:4;
then A153: M . (DG \ B0) = (M . DG) - (M . B0) by A146, MEASURE1:63;
take N0 ; :: thesis: for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n)

A154: now

let n be Nat; :: thesis: ( N0 <= n implies M . ((dom g) \ (H . n)) < e )
assume A155: N0 <= n ; :: thesis: M . ((dom g) \ (H . n)) < e
reconsider BN = H . n as Element of S by A149;
H . N0 c= H . n by A145, A155;
then M . (DG \ BN) <= M . (DG \ B0) by MEASURE1:62, XBOOLE_1:34;
hence M . ((dom g) \ (H . n)) < e by A152, A153, XXREAL_0:2; :: thesis: verum

end;

now

let n be Nat; :: thesis: ( N0 <= n implies (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) )
assume A156: N0 <= n ; :: thesis: (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n)
A157: H . n c= DG by A146;
DG = DG \/ (H . n) by A146, XBOOLE_1:12;
then A158: DG = (DG \ (H . n)) \/ (H . n) by XBOOLE_1:39;
H . n in S by A149;
then A159: X \ (H . n) in S by MEASURE1:66;
A160: DG /\ (X \ (H . n)) in S by A159, 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 A160, XBOOLE_1:28;
reconsider B = H . n as Element of S by A149;
A161: dom (F . n) = dom g by A4;
then A162: dom (F . n) = (A \/ B) /\ (dom (F . n)) by A158;
for x being set st x in dom (F . n) holds
(F . n) . x = (F . n) . x ;
then A163: F . n = (F . n) | (A \/ B) by A162, FUNCT_1:68;
A164: F . n is nonnegative by A5;
A165: ( (F . n) | A is nonnegative & (F . n) | B is nonnegative ) by A5, Th21;
A166: A misses B by XBOOLE_1:79;
A167: F . n is_simple_func_in S by A3;
A168: integral' M,(F . n) = (integral' M,((F . n) | A)) + (integral' M,((F . n) | B)) by A3, A163, A164, A166, Th73;
A169: ( (F . n) | A is_simple_func_in S & (F . n) | B is_simple_func_in S ) by A3, Th40;
( 0 <= integral' M,((F . n) | A) & 0 <= integral' M,((F . n) | B) ) by A165, A167, Th40, Th74;
then A170: integral' M,((F . n) | B) <= integral' M,(F . n) by A168, XXREAL_3:42;
dom ((F . n) | B) = (dom (F . n)) /\ B by RELAT_1:90;
then A171: dom ((F . n) | B) = B by A146, A161, XBOOLE_1:28;
consider EP being PartFunc of X,ExtREAL such that
A172: ( EP is_simple_func_in S & dom EP = B & ( for x being set st x in B holds
EP . x = e ) ) by A143, Th47;
A173: integral' M,EP = e * (M . B) by A142, A172, Th77;
A174: M . (dom g) < +infty by A127, XXREAL_0:4;
A175: 0 <= M . B by A128, A129, MEASURE1:62, XBOOLE_1:2;
A176: M . B <= M . DG by A146, MEASURE1:62;
then M . B < +infty by A127, XXREAL_0:2, XXREAL_0:4;
then e * (M . B) < e * +infty by A142, A143, XXREAL_3:83;
then A177: ( integral' M,EP <> +infty & integral' M,EP <> -infty ) by A142, A173, A175, XXREAL_0:4;
A178: ( g | B is_simple_func_in S & g | A is_simple_func_in S ) by A1, Th40;
A179: ( dom (g | A) = A & dom (g | B) = B ) by A158, RELAT_1:91, XBOOLE_1:7;
A180: ( g | A is nonnegative & g | B is nonnegative ) by B131, Th21, SUPINF_2:71;
A181: integral' M,(g | A) <> -infty by A131, A178, Th21, Th74;
A182: ((F . n) | B) + EP is_simple_func_in S by A169, A172, Th44;
for x being set st x in dom EP holds
0 <= EP . x by A142, A172;
then A183: EP is nonnegative by SUPINF_2:71;
then A184: dom (((F . n) | B) + EP) = (dom ((F . n) | B)) /\ (dom EP) by A165, A169, A172, Th71
.= B by A171, A172 ;
A185: ((F . n) | B) + EP is nonnegative by A165, A183, Th25;
A186: for x being set st x in dom ((((F . n) | B) + EP) - (g | B)) holds
(g | B) . x <= (((F . n) | B) + EP) . x

proof

let x be set ; :: thesis: ( x in dom ((((F . n) | B) + EP) - (g | B)) implies (g | B) . x <= (((F . n) | B) + EP) . x )
assume x in dom ((((F . n) | B) + EP) - (g | B)) ; :: thesis: (g | B) . x <= (((F . n) | B) + EP) . x
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 A187: x in (dom (((F . n) | B) + EP)) /\ (dom (g | B)) by XBOOLE_0:def 5;
then A188: 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 A171, A184, A188, FUNCT_1:70;
then A189: (((F . n) | B) + EP) . x = ((F . n) . x) + e by A172, A184, A188;
A190: (g | B) . x = g . x by A179, A184, A187, FUNCT_1:70;
set f = g - (F . n);
x in less_dom (g - (F . n)),e by A144, A184, A188;
then ( x in dom (g - (F . n)) & (g - (F . n)) . x < e ) by MESFUNC1:def 12;
then A193: (g . x) - ((F . n) . x) <= e by MESFUNC1:def 4;
thus (g | B) . x <= (((F . n) | B) + EP) . x by A143, A189, A190, A193, XXREAL_3:44; :: thesis: verum

end;

then A194: dom ((((F . n) | B) + EP) - (g | B)) = (dom (((F . n) | B) + EP)) /\ (dom (g | B)) by A178, A180, A182, A185, Th75;
dom (((F . n) | B) + EP) = (dom ((F . n) | B)) /\ (dom EP) by A165, A169, A172, A183, Th71;
then ( ((F . n) | B) + EP = (((F . n) | B) + EP) | (dom ((((F . n) | B) + EP) - (g | B))) & g | B = (g | B) | (dom ((((F . n) | B) + EP) - (g | B))) ) by A171, A172, A179, A194, GRFUNC_1:64;
then A195: integral' M,(g | B) <= integral' M,(((F . n) | B) + EP) by A178, A180, A182, A185, A186, Th76;
integral' M,(((F . n) | B) + EP) = (integral' M,(((F . n) | B) | B)) + (integral' M,(EP | B)) by A165, A169, A172, A183, A184, Th71
.= (integral' M,(((F . n) | B) | B)) + (integral' M,EP) by A172, GRFUNC_1:64
.= (integral' M,((F . n) | B)) + (integral' M,EP) by FUNCT_1:82 ;
then A196: (integral' M,(g | B)) - (integral' M,EP) <= integral' M,((F . n) | B) by A177, A195, XXREAL_3:45;
A197: dom g = (A \/ B) /\ (dom g) by A158;
for x being set st x in dom g holds
g . x = g . x ;
then g = g | (A \/ B) by A197, FUNCT_1:68;
then A198: integral' M,g = (integral' M,(g | A)) + (integral' M,(g | B)) by A1, A131, Th73, XBOOLE_1:79;
consider GP being PartFunc of X,ExtREAL such that
A199: ( GP is_simple_func_in S & dom GP = A & ( for x being set st x in A holds
GP . x = R_EAL (max RINGA) ) ) by Th47;
for x being set st x in dom GP holds
0 <= GP . x by A132, A199;
then A200: GP is nonnegative by SUPINF_2:71;
A201: for x being set st x in dom (GP - (g | A)) holds
(g | A) . x <= GP . x

proof

let x be set ; :: thesis: ( x in dom (GP - (g | A)) implies (g | A) . x <= GP . x )
assume x in dom (GP - (g | A)) ; :: thesis: (g | A) . x <= GP . x
then x in ((dom GP) /\ (dom (g | A))) \ (((GP " {+infty }) /\ ((g | A) " {+infty })) \/ ((GP " {-infty }) /\ ((g | A) " {-infty }))) by MESFUNC1:def 4;
then A202: x in (dom GP) /\ (dom (g | A)) by XBOOLE_0:def 5;
then A203: x in dom GP by XBOOLE_0:def 4;
A204: (g | A) . x = g . x by A179, A199, A202, FUNCT_1:70;
x in (dom g) /\ A by A179, A199, A202, RELAT_1:90;
then x in dom g by XBOOLE_0:def 4;
then g . x <= R_EAL (max RINGA) by A117;
hence (g | A) . x <= GP . x by A199, A203, A204; :: thesis: verum

end;

then dom (GP - (g | A)) = (dom GP) /\ (dom (g | A)) by A178, A180, A199, A200, Th75;
then ( (g | A) | (dom (GP - (g | A))) = g | A & GP | (dom (GP - (g | A))) = GP ) by A179, A199, GRFUNC_1:64;
then A205: integral' M,(g | A) <= integral' M,GP by A178, A180, A199, A200, A201, Th76;
A206: integral' M,GP = (R_EAL (max RINGA)) * (M . A) by A132, A199, Th77;
M . A <= M . DG by A158, MEASURE1:62, XBOOLE_1:7;
then M . A < +infty by A127, XXREAL_0:2, XXREAL_0:4;
then (R_EAL (max RINGA)) * (M . A) < (R_EAL (max RINGA)) * +infty by A132, XXREAL_3:83;
then A207: (R_EAL (max RINGA)) * (M . A) <> +infty by A132, XXREAL_3:def 5;
B208: 0 <= M . A by A128, A129, MEASURE1:62, XBOOLE_1:2;
M . A < e by A154, A156;
then A209: (R_EAL (max RINGA)) * (M . A) < (R_EAL (max RINGA)) * e by A132, XXREAL_3:83;
then A210: integral' M,(g | A) <> +infty by A205, A206, XXREAL_0:2, XXREAL_0:4;
( e <> +infty & e <> -infty ) by A142, XXREAL_0:4;
then reconsider ee = e as Real by XXREAL_0:14;
A211: (R_EAL (max RINGA)) * e = beta1 * ee by EXTREAL1:13;
A212: M . B <> -infty by A128, A129, MEASURE1:62, XBOOLE_1:2;
M . (dom g) <> -infty by A128, A129, A176, MEASURE1:62, XBOOLE_1:2;
then A213: M . (dom g) is Real by A127, XXREAL_0:14;
reconsider XSMg = integral' M,g as Real by A140, XXREAL_0:14;
reconsider XSMgA = integral' M,(g | A) as Real by A181, A210, XXREAL_0:14;
reconsider XSMGP = integral' M,GP as Real by A206, A207, B208, A132, XXREAL_0:14;
reconsider betae = (R_EAL (max RINGA)) * e as Real by A211;
reconsider XSMEP = integral' M,EP as Real by A177, XXREAL_0:14;
M . B is Real by A174, A176, A212, XXREAL_0:14;
then consider MB, MG being Real such that
A214: ( MB = M . B & MG = M . (dom g) & MB <= MG ) by A157, A213, MEASURE1:62;
A215: XSMEP = e * (M . B) by A142, A172, Th77
.= ee * MB by A214, EXTREAL1:13 ;
integral' M,(g | A) is Element of REAL by A181, A210, XXREAL_0:14;
then A216: (integral' M,g) - (integral' M,(g | A)) = integral' M,(g | B) by A198, XXREAL_3:24;
A217: (integral' M,g) - (integral' M,GP) <= (integral' M,g) - (integral' M,(g | A)) by A205, XXREAL_3:39;
X: integral' M,(g | A) is Element of REAL by A181, A210, XXREAL_0:14;
XSMg - XSMgA = (integral' M,g) - (integral' M,(g | A)) by SUPINF_2:5
.= integral' M,(g | B) by A198, X, XXREAL_3:24 ;
then reconsider XSMgB = integral' M,(g | B) as Real ;
A218: XSMg - betae < XSMg - XSMGP by A206, A209, XREAL_1:17;
(integral' M,g) - (integral' M,GP) = XSMg - XSMGP by SUPINF_2:5;
then XSMg - betae < XSMgB by A216, A217, A218, XXREAL_0:2;
then A219: (XSMg - betae) - (ee * MB) < XSMgB - XSMEP by A215, XREAL_1:16;
A220: betae = ee * beta1 by EXTREAL1:13;
ee * MB <= ee * MG by A142, A214, XREAL_1:66;
then (XSMg - betae) - (ee * MG) <= (XSMg - betae) - (ee * MB) by XREAL_1:15;
then A221: XSMg - (ee * (beta1 + MG)) < XSMgB - XSMEP by A219, A220, XXREAL_0:2;
beta1 + MG = (R_EAL (max RINGA)) + (M . (dom g)) by A214, SUPINF_2:1;
then ee * (beta1 + MG) = e * ((R_EAL (max RINGA)) + (M . (dom g))) by EXTREAL1:13;
then A222: 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 A196, A221, A222, XXREAL_0:2;
hence (integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) by A170, XXREAL_0:2; :: thesis: verum

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

end;

A223: 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: ( 0 < e & e < R_EAL (min RINGA) implies 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 )
assume ( 0 < e & e < R_EAL (min RINGA) ) ; :: thesis: 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
then consider N0 being Nat such that
A224: for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < integral' M,(F . n) by A141;

now

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

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

end;

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

let e1 be R_eal; :: thesis: ( 0 < e1 implies ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 ) )
assume A226: 0 < e1 ; :: thesis: ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 )
reconsider ralpha = R_EAL (min RINGA) as Real by XXREAL_0:14;
reconsider rdomg = M . (dom g) as Real by A130, XXREAL_0:14;
{} c= DG by XBOOLE_1:2;
then A227: 0 <= rdomg by A128, A129, MEASURE1:62;

per cases ( e1 = +infty or e1 <> +infty ) ;

suppose A228: e1 = +infty ; :: thesis: ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 )

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 A228, A116, XREAL_1:218; :: thesis: verum

end;

suppose e1 <> +infty ; :: thesis: ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 )

then reconsider re1 = e1 as Real by A226, XXREAL_0:14;
set x = re1 / (beta1 + rdomg);
set y = ralpha / 2;
A231: ralpha / 2 < ralpha by A116, XREAL_1:218;
set z = min (re1 / (beta1 + rdomg)),(ralpha / 2);

A232: now

per cases ( min (re1 / (beta1 + rdomg)),(ralpha / 2) = re1 / (beta1 + rdomg) or min (re1 / (beta1 + rdomg)),(ralpha / 2) = ralpha / 2 ) by XXREAL_0:15;

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

hence 0 < min (re1 / (beta1 + rdomg)),(ralpha / 2) by A226, A132, A227; :: thesis: verum

end;

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

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

end;

end;

end;

min (re1 / (beta1 + rdomg)),(ralpha / 2) <= ralpha / 2 by XXREAL_0:17;
then A233: min (re1 / (beta1 + rdomg)),(ralpha / 2) < ralpha by A231, XXREAL_0:2;
(min (re1 / (beta1 + rdomg)),(ralpha / 2)) * (beta1 + rdomg) <= (re1 / (beta1 + rdomg)) * (beta1 + rdomg) by A132, A227, XREAL_1:66, XXREAL_0:17;
then A234: (min (re1 / (beta1 + rdomg)),(ralpha / 2)) * (beta1 + rdomg) <= re1 by A132, A227, XCMPLX_1:88;
R_EAL (beta1 + rdomg) = (R_EAL beta1) + (R_EAL rdomg) by SUPINF_2:1;
then (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;
hence ex e being R_eal st
( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 ) by A232, A233, A234; :: thesis: verum

end;

end;

end;

A235: 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: ( 0 < e1 implies ex N0 being Nat st
for n being Nat st N0 <= n holds
(integral' M,g) - e1 < L . n )
assume 0 < e1 ; :: thesis: ex N0 being Nat st
for n being Nat st N0 <= n holds
(integral' M,g) - e1 < L . n
then consider e being R_eal such that
A236: ( 0 < e & e < R_EAL (min RINGA) & e * ((R_EAL (max RINGA)) + (M . (dom g))) <= e1 ) by A225;
consider N0 being Nat such that
A237: for n being Nat st N0 <= n holds
(integral' M,g) - (e * ((R_EAL (max RINGA)) + (M . (dom g)))) < L . n by A223, A236;
take N0 ; :: thesis: for n being Nat st N0 <= n holds
(integral' M,g) - e1 < L . n

now

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

end;

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

end;

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

proof

let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )
assume A240: n <= m ; :: thesis: L . n <= L . m
A241: ( dom (F . n) = dom g & dom (F . m) = dom g ) by A4;
A242: ( F . n is nonnegative & F . m is nonnegative ) by A5;
A243: ( F . n is_simple_func_in S & F . m is_simple_func_in S ) by A3;
A244: 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: ( x in dom ((F . m) - (F . n)) implies (F . n) . x <= (F . m) . x )
assume x in dom ((F . m) - (F . n)) ; :: thesis: (F . n) . x <= (F . m) . x
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, A240, A241; :: thesis: verum

end;

then A245: integral' M,((F . n) | (dom ((F . m) - (F . n)))) <= integral' M,((F . m) | (dom ((F . m) - (F . n)))) by A242, A243, Th76;
dom ((F . m) - (F . n)) = (dom (F . m)) /\ (dom (F . n)) by A242, A243, A244, Th75;
then ( (F . m) | (dom ((F . m) - (F . n))) = F . m & (F . n) | (dom ((F . m) - (F . n))) = F . n ) by A241, GRFUNC_1:64;
then L . n <= integral' M,(F . m) by A8, A245;
hence L . n <= L . m by A8; :: thesis: verum

end;

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

proof

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

end;

per cases ( ex K being real number st
( 0 < K & ( for n being Nat holds L . n < K ) ) or for K being real number holds
( not 0 < K or ex n being Nat st not L . n < K ) ) ;

suppose ex K being real number st
( 0 < K & ( for n being Nat holds L . n < K ) ) ; :: thesis: ( L is convergent & integral' M,g <= lim L )

then consider K being real number such that
0 < K and
A247: for n being Nat holds L . n < K ;
A248: for n being Nat holds L . n <= sup (rng L)

proof

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

end;

then L . 1 <= sup (rng L) ;
then A250: sup (rng L) <> -infty by A246;
R_EAL K is UpperBound of rng L

proof

now

let x be ext-real number ; :: thesis: ( x in rng L implies x <= R_EAL K )
assume x in rng L ; :: thesis: x <= R_EAL K
then consider z being set such that
A251: z in dom L and
A252: x = L . z by FUNCT_1:def 5;
thus x <= R_EAL K by A247, A251, A252; :: thesis: verum

end;

hence R_EAL K is UpperBound of rng L by XXREAL_2:def 1; :: thesis: verum

end;

then A253: sup (rng L) <= R_EAL K by XXREAL_2:def 3;
R_EAL K is Real by XREAL_0:def 1;
then A254: sup (rng L) <> +infty by A253, XXREAL_0:9;
A255: 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: ( 0 < p implies ex N0 being Nat st
for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p )
assume A256: 0 < p ; :: thesis: ex N0 being Nat st
for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p
sup (rng L) is Real by A250, A254, XXREAL_0:14;
then consider y being ext-real number such that
A257: ( y in rng L & (sup (rng L)) - (R_EAL p) < y ) by A256, MEASURE6:33;
consider x being set such that
A258: ( x in dom L & y = L . x ) by A257, FUNCT_1:def 5;
reconsider N0 = x as Element of NAT by A258;
take N0 ; :: thesis: for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p
let n be Nat; :: thesis: ( N0 <= n implies |.((L . n) - (sup (rng L))).| < p )
assume N0 <= n ; :: thesis: |.((L . n) - (sup (rng L))).| < p
then L . N0 <= L . n by A239;
then A259: (sup (rng L)) - (R_EAL p) < L . n by A257, A258, XXREAL_0:2;
A260: L . n <= sup (rng L) by A248;
(sup (rng L)) + 0. <= (sup (rng L)) + (R_EAL p) by A256, XXREAL_3:38;
then A261: sup (rng L) <= (sup (rng L)) + (R_EAL p) by XXREAL_3:4;
sup (rng L) <> (sup (rng L)) + (R_EAL p)

proof

assume A262: sup (rng L) = (sup (rng L)) + (R_EAL p) ; :: thesis: contradiction
((R_EAL p) + (sup (rng L))) + (- (sup (rng L))) = (R_EAL p) + ((sup (rng L)) + (- (sup (rng L)))) by A250, A254, XXREAL_3:30
.= (R_EAL p) + 0 by XXREAL_3:7
.= R_EAL p by XXREAL_3:4 ;
hence contradiction by A256, A262, XXREAL_3:7; :: thesis: verum

end;

then sup (rng L) < (sup (rng L)) + (R_EAL p) by A261, XXREAL_0:1;
then L . n < (sup (rng L)) + (R_EAL p) by A260, XXREAL_0:2;
then A263: (L . n) - (sup (rng L)) < R_EAL p by XXREAL_3:66;
sup (rng L) < (L . n) + (R_EAL p) by A259, 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 - (R_EAL p) < (L . n) - (sup (rng L)) by XXREAL_3:27;
hence |.((L . n) - (sup (rng L))).| < p by A263, EXTREAL2:59; :: thesis: verum

end;

reconsider h = sup (rng L) as Real by A250, A254, XXREAL_0:14;
A264: R_EAL h = sup (rng L) ;
then A265: L is convergent_to_finite_number by A255, Def8;
hence L is convergent by Def11; :: thesis: integral' M,g <= lim L
then A266: lim L = sup (rng L) by A255, A264, A265, Def12;

now

let e be real number ; :: thesis: ( 0 < e implies integral' M,g < (lim L) + e )
assume 0 < e ; :: thesis: integral' M,g < (lim L) + e
then consider N0 being Nat such that
A267: for n being Nat st N0 <= n holds
(integral' M,g) - (R_EAL e) < L . n by A235;
A268: (integral' M,g) - (R_EAL e) < L . N0 by A267;
L . N0 <= sup (rng L) by A248;
then (integral' M,g) - (R_EAL e) < sup (rng L) by A268, XXREAL_0:2;
hence integral' M,g < (lim L) + e by A266, XXREAL_3:65; :: thesis: verum

end;

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

end;

suppose A269: for K being real number holds
( not 0 < K or ex n being Nat st not L . n < K ) ; :: thesis: ( L is convergent & integral' M,g <= lim L )

now

let K be real number ; :: thesis: ( 0 < K implies ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n )
assume 0 < K ; :: thesis: ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n
then consider N0 being Nat such that
A270: R_EAL K <= L . N0 by A269;

now

let n be Nat; :: thesis: ( N0 <= n implies R_EAL K <= L . n )
assume N0 <= n ; :: thesis: R_EAL K <= L . n
then L . N0 <= L . n by A239;
hence R_EAL K <= L . n by A270, XXREAL_0:2; :: thesis: verum

end;

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

end;

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

end;

end;

end;

suppose A272: M . (dom g) = +infty ; :: thesis: ( L is convergent & integral' M,g <= lim L )

reconsider DG = dom g as Element of S by A1, Th43;
A273: 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: ( 0 < e & e < R_EAL (min RINGA) implies for n being Nat holds ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n) )
assume A274: ( 0 < e & e < R_EAL (min RINGA) ) ; :: thesis: for n being Nat holds ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n)
then A275: ( e <> -infty & e <> +infty ) by XXREAL_0:4;
A276: 0 <= (R_EAL (min RINGA)) - e by A274, XXREAL_3:43;
consider H being SetSequence of X, MF being ExtREAL_sequence such that
A277: 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
A278: 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
A279: for n being Nat holds H . n in S by A37, A274;

now

let n be Nat; :: thesis: ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n)
A280: DG = DG \/ (H . n) by A278, XBOOLE_1:12
.= (DG \ (H . n)) \/ (H . n) by XBOOLE_1:39 ;
H . n in S by A279;
then A281: 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 A281, MEASURE1:66;
reconsider B = H . n as Element of S by A279;
A283: dom (F . n) = dom g by A4;
then A284: dom (F . n) = (A \/ B) /\ (dom (F . n)) by A280;
for x being set st x in dom (F . n) holds
(F . n) . x = (F . n) . x ;
then A285: F . n = (F . n) | (A \/ B) by A284, FUNCT_1:68;
A286: F . n is nonnegative by A5;
A287: A misses B by XBOOLE_1:79;
A288: F . n is_simple_func_in S by A3;
A289: integral' M,(F . n) = (integral' M,((F . n) | A)) + (integral' M,((F . n) | B)) by A3, A285, A286, A287, Th73;
A290: ( (F . n) | A is nonnegative & (F . n) | B is nonnegative ) by A5, Th21;
A291: ( (F . n) | A is_simple_func_in S & (F . n) | B is_simple_func_in S ) by A3, Th40;
( 0 <= integral' M,((F . n) | A) & 0 <= integral' M,((F . n) | B) ) by A288, A290, Th40, Th74;
then A292: integral' M,((F . n) | B) <= integral' M,(F . n) by A289, XXREAL_3:42;
A293: dom ((F . n) | B) = (dom (F . n)) /\ B by RELAT_1:90
.= B by A280, A283, XBOOLE_1:7, XBOOLE_1:28 ;
consider EP being PartFunc of X,ExtREAL such that
A294: ( EP is_simple_func_in S & dom EP = B & ( for x being set st x in B holds
EP . x = (R_EAL (min RINGA)) - e ) ) by A276, Th47, A274, XXREAL_3:18;
for x being set st x in dom EP holds
0 <= EP . x by A276, A294;
then A295: EP is nonnegative by SUPINF_2:71;
A296: for x being set st x in dom (((F . n) | B) - EP) holds
EP . x <= ((F . n) | B) . x

proof

let x be set ; :: thesis: ( x in dom (((F . n) | B) - EP) implies EP . x <= ((F . n) | B) . x )
assume x in dom (((F . n) | B) - EP) ; :: thesis: EP . x <= ((F . n) | B) . x
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 A297: x in (dom ((F . n) | B)) /\ (dom EP) by XBOOLE_0:def 5;
then A298: x in dom ((F . n) | B) by XBOOLE_0:def 4;
then A299: ((F . n) | B) . x = (F . n) . x by FUNCT_1:70;
set f = g - (F . n);
A300: dom (g - (F . n)) = dom g by A34;
x in less_dom (g - (F . n)),e by A277, A293, A298;
then A301: ( x in dom (g - (F . n)) & (g - (F . n)) . x < e ) by MESFUNC1:def 12;
then A302: (g . x) - ((F . n) . x) <= e by MESFUNC1:def 4;
g . x <= ((F . n) . x) + e by A275, A302, XXREAL_3:44;
then A303: (g . x) - e <= (F . n) . x by A275, XXREAL_3:45;
R_EAL (min RINGA) <= g . x by A117, A300, A301;
then (R_EAL (min RINGA)) - e <= (g . x) - e by XXREAL_3:39;
then (R_EAL (min RINGA)) - e <= (F . n) . x by A303, XXREAL_0:2;
hence EP . x <= ((F . n) | B) . x by A293, A294, A297, A299; :: thesis: verum

end;

then A304: integral' M,(EP | (dom (((F . n) | B) - EP))) <= integral' M,(((F . n) | B) | (dom (((F . n) | B) - EP))) by A290, A291, A294, A295, Th76;
A305: integral' M,EP = ((R_EAL (min RINGA)) - e) * (M . B) by A274, A294, Th77, XXREAL_3:43;
dom (((F . n) | B) - EP) = (dom ((F . n) | B)) /\ (dom EP) by A290, A291, A294, A295, A296, Th75;
then ( EP | (dom (((F . n) | B) - EP)) = EP & ((F . n) | B) | (dom (((F . n) | B) - EP)) = (F . n) | B ) by A293, A294, GRFUNC_1:64;
then integral' M,EP <= integral' M,(F . n) by A292, A304, XXREAL_0:2;
hence ((R_EAL (min RINGA)) - e) * (M . (less_dom (g - (F . n)),e)) <= integral' M,(F . n) by A277, A305; :: thesis: verum

end;

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

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

let y be real number ; :: thesis: ( 0 < y implies ex n being Nat st
for m being Nat st n <= m holds
y <= L . m )
assume 0 < y ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
y <= L . m
set e = (R_EAL (min RINGA)) / (R_EAL 2);
reconsider ralpha = R_EAL (min RINGA) as Real by XXREAL_0:14;
set a2 = ralpha / 2;
A306: (R_EAL (min RINGA)) / (R_EAL 2) = ralpha / 2 by EXTREAL1:39;
A309: (R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2)) = ralpha - (ralpha / 2) by A306, SUPINF_2:5;
(ralpha / 2) - (ralpha / 2) < ralpha - (ralpha / 2) by A116;
then A311: 0 < (R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2)) by A306, SUPINF_2:5;
reconsider y1 = y as Real by XREAL_0:def 1;
y = (ralpha - (ralpha / 2)) * (y1 / (ralpha - (ralpha / 2))) by A116, XCMPLX_1:88;
then y = (R_EAL (ralpha - (ralpha / 2))) * (R_EAL (y1 / (ralpha - (ralpha / 2)))) by EXTREAL1:38;
then A312: ((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 A309, EXTREAL1:39;
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 A306, SUPINF_2:5 ;
then A313: (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) < +infty by XXREAL_0:9;
consider H being SetSequence of X, MF being ExtREAL_sequence such that
A314: for n being Nat holds H . n = less_dom (g - (F . n)),((R_EAL (min RINGA)) / (R_EAL 2)) and
A315: 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
A316: for n being Nat holds MF . n = M . (H . n) and
A317: M . (dom g) = sup (rng MF) and
A318: for n being Nat holds H . n in S by A37, A116, A306, XREAL_1:218;
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: contradiction
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 A272, A313, A317, XXREAL_2:def 3; :: thesis: verum

end;

then consider z being R_eal such that
A319: ( z in rng MF & (R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) <= z ) ;
consider x being set such that
A320: ( x in dom MF & z = MF . x ) by A319, FUNCT_1:def 5;
reconsider N0 = x as Element of NAT by A320;
take N0 ; :: thesis: for m being Nat st N0 <= m holds
y <= L . m
thus for m being Nat st N0 <= m holds
y <= L . m :: thesis: verum

proof

let m be Nat; :: thesis: ( N0 <= m implies y <= L . m )
assume A321: N0 <= m ; :: thesis: y <= L . m
(R_EAL y) / ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) <= M . (H . N0) by A316, A319, A320;
then A322: R_EAL y <= ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (H . N0)) by A311, A312, XXREAL_3:82;
A323: H . N0 c= H . m by A315, A321;
( H . N0 in S & H . m in S ) by A318;
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 A311, A323, MEASURE1:62, XXREAL_3:82;
then R_EAL y <= ((R_EAL (min RINGA)) - ((R_EAL (min RINGA)) / (R_EAL 2))) * (M . (H . m)) by A322, XXREAL_0:2;
then A324: 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 A314;
((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 A273, A116, A306, XREAL_1:218;
then R_EAL y <= integral' M,(F . m) by A324, XXREAL_0:2;
hence y <= L . m by A8; :: thesis: verum

end;

end;

then A325: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis: integral' M,g <= lim L
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 A325, Th56, XXREAL_0:4; :: thesis: verum

end;

end;

end;

end;