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 object 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 object 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 object 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 object 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 object 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 object 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 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: ( L is convergent & integral' (M,g) <= lim L )

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 object 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 object 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 object 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 object 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 object 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 object 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 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: ( L is convergent & integral' (M,g) <= lim L )

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

end;

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

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

lim L = 0 by A10, Th52;

hence integral' (M,g) <= lim L by A9, Def14; :: thesis: verum

end;

A10: now :: thesis: for n being Nat holds L . n = 0

then
L is convergent_to_finite_number
by Th52;let n be Nat; :: thesis: L . n = 0

dom (F . n) = {} by A4, A9;

then integral' (M,(F . n)) = 0 by Def14;

hence L . n = 0 by A8; :: thesis: verum

end;dom (F . n) = {} by A4, A9;

then integral' (M,(F . n)) = 0 by Def14;

hence L . n = 0 by A8; :: thesis: verum

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

lim L = 0 by A10, Th52;

hence integral' (M,g) <= lim L by A9, Def14; :: thesis: verum

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

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_{1}[ 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_{1}[k,x]

A22: ( dom a1 = Seg (len a) & ( for k being Nat st k in Seg (len a) holds

S_{1}[k,a1 . k] ) )
from FINSEQ_1:sch 5(A15);

A23: len a <> 0

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 )

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 ) )

end;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

A15: for k being Nat st k in Seg (len a) holds

ex x being Element of REAL st S

proof

consider a1 being FinSequence of REAL such that
let k be Nat; :: thesis: ( k in Seg (len a) implies ex x being Element of REAL st S_{1}[k,x] )

assume A16: k in Seg (len a) ; :: thesis: ex x being Element of REAL st S_{1}[k,x]

then A17: 1 <= k by FINSEQ_1:1;

A18: k in dom a by A16, FINSEQ_1:def 3;

end;assume A16: k in Seg (len a) ; :: thesis: ex x being Element of REAL st S

then A17: 1 <= k by FINSEQ_1:1;

A18: k in dom a by A16, FINSEQ_1:def 3;

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

end;

suppose A19:
k = 1
; :: thesis: ex x being Element of REAL st S_{1}[k,x]

take
In (0,REAL)
; :: thesis: S_{1}[k, In (0,REAL)]

thus S_{1}[k, In (0,REAL)]
by A13, A19; :: thesis: verum

end;thus S

suppose
k <> 1
; :: thesis: ex x being Element of REAL st S_{1}[k,x]

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: S_{1}[k,x]

thus S_{1}[k,x]
; :: thesis: verum

end;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: S

thus S

A22: ( dom a1 = Seg (len a) & ( for k being Nat st k in Seg (len a) holds

S

A23: len a <> 0

proof

A28:
2 <= len a
assume
len a = 0
; :: thesis: contradiction

then A24: dom a = Seg 0 by FINSEQ_1:def 3;

A25: rng G = {}

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

end;then A24: dom a = Seg 0 by FINSEQ_1:def 3;

A25: rng G = {}

proof

union (rng G) <> {}
by A11, A12, MESFUNC3:def 1;
assume
rng G <> {}
; :: thesis: contradiction

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

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

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

proof

then
1 <= len a
by XXREAL_0:2;
assume
not 2 <= len a
; :: thesis: contradiction

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

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

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

A56:
for n being Nat holds dom (g - (F . n)) = dom g
let x be set ; :: thesis: ( x in dom g implies ( alpha <= g . x & g . x <= beta ) )

assume A45: x in dom g ; :: thesis: ( alpha <= g . x & g . x <= beta )

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;

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

end;assume A45: x in dom g ; :: thesis: ( alpha <= g . x & g . x <= beta )

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: not a1 . k = a1 . 1

then A54:
not a1 . k in {(a1 . 1)}
by TARSKI:def 1;
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: contradiction

a . k = a1 . k by A22, A50;

then a . k = a . 1 by A22, A53, A51;

hence contradiction by A2, A13, A45, A52; :: thesis: verum

end;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: contradiction

a . k = a1 . k by A22, A50;

then a . k = a . 1 by A22, A53, A51;

hence contradiction by A2, A13, A45, A52; :: thesis: verum

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

proof

A60:
g is real-valued
by A1, MESFUNC2:def 4;
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: dom (g - (F . n)) = dom g

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

end;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: dom (g - (F . n)) = dom g

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

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: ( 0 < e & e < alpha 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 that

A62: 0 < e and

A63: e < alpha ; :: 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_{1}( 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_{1}(n)
from FUNCT_2:sch 4();

deffunc H_{2}( 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_{2}(n)
from FUNCT_2:sch 4();

A104: for n, m being Nat st n <= m holds

H . n c= H . m

H . n c= H . m ;

then A113: H is non-descending by PROB_1:def 5;

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 ) )

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

end;( ( 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 that

A62: 0 < e and

A63: e < alpha ; :: 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

consider H being SetSequence of X such that

A64: for n being Element of NAT holds H . n = H

A65: now :: thesis: for n being Nat holds H . n = H_{1}(n)

A66:
for n being Nat holds H . n c= dom g
let n be Nat; :: thesis: H . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

hence H . n = H_{1}(n)
by A64; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence H . n = H

proof

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

end;now :: thesis: for x being object st x in H . n holds

x in dom g

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

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

then x in dom (g - (F . n)) by MESFUNC1:def 11;

hence x in dom g by A56; :: thesis: verum

end;assume x in H . n ; :: thesis: x in dom g

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

proof

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

end;assume x in Union H ; :: thesis: x in dom g

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

now :: thesis: for x being object st x in dom g holds

x in lim_inf H

then A101:
dom g c= lim_inf H
;x in lim_inf H

let x be object ; :: thesis: ( x in dom g implies x in lim_inf H )

assume A69: x in dom g ; :: thesis: x in lim_inf H

then reconsider x1 = x as Element of X ;

A70: F # x1 is convergent by A7, A69;

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

end;assume A69: x in dom g ; :: thesis: x in lim_inf H

then reconsider x1 = x as Element of X ;

A70: F # x1 is convergent by A7, A69;

A71: now :: thesis: not F # x1 is convergent_to_-infty

reconsider E = e as Element of REAL by A62, A63, XXREAL_0:48;

assume F # x1 is convergent_to_-infty ; :: thesis: contradiction

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

end;assume F # x1 is convergent_to_-infty ; :: thesis: contradiction

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

now :: thesis: ex N being Nat st

( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N )end;

then consider N being Nat such that ( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N )

per cases
( F # x1 is convergent_to_finite_number or F # x1 is convergent_to_+infty )
by A70, A71;

end;

suppose A74:
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 )

( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N )

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;

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

end;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: for k being Nat holds x in H . (N + k)

then A87:
x in (inferior_setsequence H) . N
by SETLIM_1:19;let k be Nat; :: thesis: x in H . (N + k)

set m = N + k;

A78: x1 in dom (g - (F . (N + k))) by A56, A69;

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

end;set m = N + k;

A78: x1 in dom (g - (F . (N + k))) by A56, A69;

now :: thesis: for e being Real st 0 < e holds

(F # x1) . (N + k) < (lim (F # x1)) + e

then
(F # x1) . (N + k) <= lim (F # x1)
by XXREAL_3:61;(F # x1) . (N + k) < (lim (F # x1)) + e

let e be Real; :: 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

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

end;assume 0 < e ; :: thesis: (F # x1) . (N + k) < (lim (F # x1)) + e

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

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

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

suppose A88:
F # x1 is convergent_to_+infty
; :: thesis: ex N being Nat st

( N in dom (inferior_setsequence H) & x in (inferior_setsequence H) . N )

( 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

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;

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

end;for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

proof

then consider N being Nat such that
A89:
e in REAL
by A62, A63, XXREAL_0:48;

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

end;

suppose A90:
(g . x1) - e <= 0
; :: thesis: ex N being Nat st

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

consider N being Nat such that

A91: for m being Nat st N <= m holds

1 <= (F # x1) . m by A88;

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e ; :: thesis: verum

end;A91: for m being Nat st N <= m holds

1 <= (F # x1) . m by A88;

now :: thesis: for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

hence
ex N being Nat st (g . x1) - ((F . m) . x1) < e

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

end;assume N <= m ; :: thesis: (g . x1) - ((F . m) . x1) < e

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

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e ; :: thesis: verum

suppose A92:
0 < (g . x1) - e
; :: thesis: ex N being Nat st

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

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;

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e ; :: thesis: verum

end;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: for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e

hence
ex N being Nat st (g . x1) - ((F . m) . x1) < e

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

end;assume N <= m ; :: thesis: (g . x1) - ((F . m) . x1) < e

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

for m being Nat st N <= m holds

(g . x1) - ((F . m) . x1) < e ; :: thesis: verum

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: for m being Nat st N <= m holds

x1 in less_dom ((g - (F . m)),e)

x1 in less_dom ((g - (F . m)),e)

let m be Nat; :: thesis: ( N <= m implies x1 in less_dom ((g - (F . m)),e) )

A97: x1 in dom (g - (F . m)) by A56, A69;

assume N <= m ; :: thesis: x1 in less_dom ((g - (F . m)),e)

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

end;A97: x1 in dom (g - (F . m)) by A56, A69;

assume N <= m ; :: thesis: x1 in less_dom ((g - (F . m)),e)

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

now :: thesis: for k being Nat holds x in H . (N + k)

then A98:
x in (inferior_setsequence H) . N
by SETLIM_1:19;let k be Nat; :: thesis: x in H . (N + k)

x in less_dom ((g - (F . (N + k))),e) by A96, NAT_1:11;

hence x in H . (N + k) by A65; :: thesis: verum

end;x in less_dom ((g - (F . (N + k))),e) by A96, NAT_1:11;

hence x in H . (N + k) by A65; :: thesis: verum

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

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

deffunc H

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

A104: for n, m being Nat st n <= m holds

H . n c= H . m

proof

then
for n, m being Nat st n <= m holds
let n, m be Nat; :: thesis: ( n <= m implies H . n c= H . m )

assume A105: n <= m ; :: thesis: H . n c= H . m

end;assume A105: n <= m ; :: thesis: H . n c= H . m

now :: thesis: for x being object st x in H . n holds

x in H . m

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

let x be object ; :: thesis: ( x in H . n implies x in H . m )

assume x in H . n ; :: thesis: x in H . m

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

end;assume x in H . n ; :: thesis: x in H . m

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

H . n c= H . m ;

then A113: H is non-descending by PROB_1:def 5;

A114: now :: thesis: for n being Nat holds MF . n = H_{2}(n)

let n be Nat; :: thesis: MF . n = H_{2}(n)

n in NAT by ORDINAL1:def 12;

hence MF . n = H_{2}(n)
by A103; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence MF . n = H

now :: thesis: for x being object st x in lim_inf H holds

x in dom g

then
lim_inf H c= dom g
;x in dom g

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

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

end;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

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

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

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 ) )

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

end;

A121: now :: thesis: for x being object st x in NAT holds

H . x in S

dom H = NAT
by FUNCT_2:def 1;H . x in S

reconsider E = e as Element of REAL by A62, A63, XXREAL_0:48;

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

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

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

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

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

for x being object st x in dom MF holds
let x be object ; :: thesis: ( x in dom MF iff ( x in dom H & H . x in dom M ) )

end;now :: thesis: ( x in dom MF implies ( x in dom H & H . x in dom M ) )

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

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

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

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

now :: thesis: for n being Nat holds H . n in S

hence
ex H being SetSequence of X ex MF being ExtREAL_sequence st let n be Nat; :: thesis: H . n in S

n in NAT by ORDINAL1:def 12;

hence H . n in S by A120; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence H . n in S by A120; :: thesis: verum

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

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

end;

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

A137:
0 < beta

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)

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))

ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - e1 < L . n

L . n <= L . m

end;proof

A140:
{} in S
by MEASURE1:34;
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: verum

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

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

beta * (M . DG) = beta1 * MG
by EXTREAL1:1;
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

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

end;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

for x being object st x in dom GP holds
let x be object ; :: 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 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: verum

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

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

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

A249:
for e being R_eal st 0 < e & e < alpha holds
let e be R_eal; :: thesis: ( 0 < e & e < alpha implies 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)) )

assume that

A158: 0 < e and

A159: e < alpha ; :: thesis: 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))

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: for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n))

(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;

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n)) ; :: thesis: verum

end;for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n)) )

assume that

A158: 0 < e and

A159: e < alpha ; :: thesis: 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))

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: for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n))

(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: for n being Nat st N0 <= n holds

M . ((dom g) \ (H . n)) < e

M . ((dom g) \ (H . n)) < e

let n be Nat; :: thesis: ( N0 <= n implies M . ((dom g) \ (H . n)) < e )

reconsider BN = H . n as Element of S by A166;

assume N0 <= n ; :: thesis: M . ((dom g) \ (H . n)) < e

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

end;reconsider BN = H . n as Element of S by A166;

assume N0 <= n ; :: thesis: M . ((dom g) \ (H . n)) < e

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

now :: thesis: for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n))

hence
for n being Nat st N0 <= n holds (integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n))

reconsider XSMg = integral' (M,g) as Element of REAL by A156, A144, XXREAL_0:14;

let n be Nat; :: thesis: ( N0 <= n implies (integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n)) )

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

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: (integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n))

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

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

end;let n be Nat; :: thesis: ( N0 <= n implies (integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n)) )

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

for x being object st x in dom GP holds
let x be object ; :: 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 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: verum

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

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: (integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n))

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

A243:
((F . n) | B) + EP is nonnegative
by A232, A215, Th19;
set f = g - (F . n);

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

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

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

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < integral' (M,(F . n)) ; :: thesis: verum

ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

proof

A253:
for e1 being R_eal st 0 < e1 holds
let e be R_eal; :: thesis: ( 0 < e & e < alpha implies ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n )

assume that

A250: 0 < e and

A251: e < alpha ; :: thesis: ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

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;

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n ; :: thesis: verum

end;for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n )

assume that

A250: 0 < e and

A251: e < alpha ; :: thesis: ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

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: for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

hence
ex N0 being Nat st (integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

let n be Nat; :: thesis: ( N0 <= n implies (integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n )

assume N0 <= n ; :: thesis: (integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

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

end;assume N0 <= n ; :: thesis: (integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n

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

for n being Nat st N0 <= n holds

(integral' (M,g)) - (e * (beta + (M . (dom g)))) < L . n ; :: thesis: verum

ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

proof

A262:
for e1 being R_eal st 0 < e1 holds
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: ( 0 < e1 implies ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 ) )

assume A254: 0 < e1 ; :: thesis: ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

{} c= DG ;

then A255: 0 <= rdomg by A141, A140, MEASURE1:31;

end;reconsider rdomg = M . (dom g) as Element of REAL by A136, A142, XXREAL_0:14;

let e1 be R_eal; :: thesis: ( 0 < e1 implies ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 ) )

assume A254: 0 < e1 ; :: thesis: ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

{} c= DG ;

then A255: 0 <= rdomg by A141, A140, MEASURE1:31;

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

end;

suppose A256:
e1 = +infty
; :: thesis: ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

reconsider z = ralpha / 2 as R_eal ;

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

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

suppose
e1 <> +infty
; :: thesis: ex e being R_eal st

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

( 0 < e & e < alpha & e * (beta + (M . (dom g))) <= e1 )

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 ;

take z ; :: thesis: ( 0 < z & z < alpha & z * (beta + (M . (dom g))) <= e1 )

hence ( 0 < z & z < alpha & z * (beta + (M . (dom g))) <= e1 ) by A261, A258, A259; :: thesis: verum

end;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 ;

take z ; :: thesis: ( 0 < z & z < alpha & z * (beta + (M . (dom g))) <= e1 )

A261: now :: thesis: 0 < z

z * (beta1 + rdomg) <= re1
by A137, A255, XCMPLX_1:87, A260;end;

hence ( 0 < z & z < alpha & z * (beta + (M . (dom g))) <= e1 ) by A261, A258, A259; :: thesis: verum

ex N0 being Nat st

for n being Nat st N0 <= n holds

(integral' (M,g)) - e1 < L . n

proof

A268:
for n being Nat holds 0 <= L . n
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

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: for n being Nat st N0 <= n holds

(integral' (M,g)) - e1 < L . n

(integral' (M,g)) - e1 < L . n ; :: thesis: verum

end;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

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: for n being Nat st N0 <= n holds

(integral' (M,g)) - e1 < L . n

now :: thesis: for n being Nat st N0 <= n holds

(integral' (M,g)) - e1 < L . n

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

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

end;assume N0 <= n ; :: thesis: (integral' (M,g)) - e1 < L . n

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

(integral' (M,g)) - e1 < L . n ; :: thesis: verum

proof

A269:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: 0 <= L . n

F . n is nonnegative by A5;

then 0 <= integral' (M,(F . n)) by A3, Th68;

hence 0 <= L . n by A8; :: thesis: verum

end;F . n is nonnegative by A5;

then 0 <= integral' (M,(F . n)) by A3, Th68;

hence 0 <= L . n by A8; :: thesis: verum

L . n <= L . m

proof

let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )

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: L . n <= L . m

A274: for x being object st x in dom ((F . m) - (F . n)) holds

(F . n) . x <= (F . m) . x

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

end;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: L . n <= L . m

A274: for x being object st x in dom ((F . m) - (F . n)) holds

(F . n) . x <= (F . m) . x

proof

A275:
F . n is_simple_func_in S
by A3;
let x be object ; :: 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, A273, A270, A272; :: thesis: verum

end;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, A273, A270, A272; :: thesis: verum

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

per cases
( ex K being Real st

( 0 < K & ( for n being Nat holds L . n < K ) ) or for K being Real holds

( not 0 < K or ex n being Nat st not L . n < K ) ) ;

end;

( 0 < K & ( for n being Nat holds L . n < K ) ) or for K being Real holds

( not 0 < K or ex n being Nat st not L . n < K ) ) ;

suppose
ex K being Real st

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

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

then consider K being Real such that

0 < K and

A281: for n being Nat holds L . n < K ;

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)

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

then A298: L is convergent_to_finite_number by A287;

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

then A299: lim L = sup (rng L) by A287, A297, A298, Def12;

end;0 < K and

A281: for n being Nat holds L . n < K ;

now :: thesis: for x being ExtReal st x in rng L holds

x <= K

then
K is UpperBound of rng L
by XXREAL_2:def 1;x <= K

let x be ExtReal; :: thesis: ( x in rng L implies x <= K )

assume x in rng L ; :: thesis: x <= K

then ex z being object st

( z in dom L & x = L . z ) by FUNCT_1:def 3;

hence x <= K by A281; :: thesis: verum

end;assume x in rng L ; :: thesis: x <= K

then ex z being object st

( z in dom L & x = L . z ) by FUNCT_1:def 3;

hence x <= K by A281; :: thesis: verum

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

then
L . 1 <= sup (rng L)
;
let n be Nat; :: thesis: L . n <= sup (rng L)

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

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

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

A297:
h = sup (rng L)
;
let p be Real; :: thesis: ( 0 < p implies ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p )

assume A288: 0 < p ; :: thesis: ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p

A289: sup (rng L) <> (sup (rng L)) + p

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

end;for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p )

assume A288: 0 < p ; :: thesis: ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p

A289: sup (rng L) <> (sup (rng L)) + p

proof

sup (rng L) in REAL
by A286, A283, XXREAL_0:14;
assume A290:
sup (rng L) = (sup (rng L)) + p
; :: thesis: contradiction

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

end;(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: verum

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

then A298: L is convergent_to_finite_number by A287;

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

then A299: lim L = sup (rng L) by A287, A297, A298, Def12;

now :: thesis: for e being Real st 0 < e holds

integral' (M,g) < (lim L) + e

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

let e be Real; :: thesis: ( 0 < e implies integral' (M,g) < (lim L) + e )

assume A300: 0 < e ; :: thesis: integral' (M,g) < (lim L) + e

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

end;assume A300: 0 < e ; :: thesis: integral' (M,g) < (lim L) + e

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

suppose A303:
for K being Real holds

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

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

then lim L = +infty by A305, Def12;

hence integral' (M,g) <= lim L by XXREAL_0:4; :: thesis: verum

end;

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

now :: thesis: for K being Real st 0 < K holds

ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n

then A305:
L is convergent_to_+infty
;ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n

let K be Real; :: 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

A304: K <= L . N0 by A303;

for n being Nat st N0 <= n holds

K <= L . n ; :: thesis: verum

end;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

A304: K <= L . N0 by A303;

now :: thesis: for n being Nat st N0 <= n holds

K <= L . n

hence
ex N0 being Nat st K <= L . n

let n be Nat; :: thesis: ( N0 <= n implies K <= L . n )

assume N0 <= n ; :: thesis: K <= L . n

then L . N0 <= L . n by A269;

hence K <= L . n by A304, XXREAL_0:2; :: thesis: verum

end;assume N0 <= n ; :: thesis: K <= L . n

then L . N0 <= L . n by A269;

hence K <= L . n by A304, XXREAL_0:2; :: thesis: verum

for n being Nat st N0 <= n holds

K <= L . n ; :: thesis: verum

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

then lim L = +infty by A305, Def12;

hence integral' (M,g) <= lim L by XXREAL_0:4; :: thesis: verum

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

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))

ex n being Nat st

for m being Nat st n <= m holds

y <= L . m

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

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

end;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

for y being Real st 0 < y holds
let e be R_eal; :: thesis: ( 0 < e & e < alpha implies for n being Nat holds (alpha - e) * (M . (less_dom ((g - (F . n)),e))) <= integral' (M,(F . n)) )

assume that

A308: 0 < e and

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

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;

end;assume that

A308: 0 < e and

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

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: for n being Nat holds (alpha - e) * (M . (less_dom ((g - (F . n)),e))) <= integral' (M,(F . n))

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

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

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

end;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

A332:
F . n is_simple_func_in S
by A3;
set f = g - (F . n);

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

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

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

ex n being Nat st

for m being Nat st n <= m holds

y <= L . m

proof

then A361:
L is convergent_to_+infty
;
reconsider ralpha = alpha as Real ;

reconsider e = alpha / 2 as R_eal ;

let y be Real; :: 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 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 )

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: for m being Nat st N0 <= m holds

y <= L . m

A356: (alpha - e) * (y / (alpha - e)) = y by A342;

thus for m being Nat st N0 <= m holds

y <= L . m :: thesis: verum

end;reconsider e = alpha / 2 as R_eal ;

let y be Real; :: 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 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

then consider z being R_eal such that
assume
for z being ExtReal holds

( not z in rng MF or not y / (alpha - e) <= z ) ; :: thesis: contradiction

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

end;( not z in rng MF or not y / (alpha - e) <= z ) ; :: thesis: contradiction

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

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: for m being Nat st N0 <= m holds

y <= L . m

A356: (alpha - e) * (y / (alpha - e)) = y by A342;

thus for m being Nat st N0 <= m holds

y <= L . m :: thesis: verum

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: ( N0 <= m implies y <= L . m )

A358: H . m in S by A348;

assume N0 <= m ; :: thesis: y <= L . m

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

end;then A357: y <= (alpha - e) * (M . (H . N0)) by A353, A356, XXREAL_3:71;

let m be Nat; :: thesis: ( N0 <= m implies y <= L . m )

A358: H . m in S by A348;

assume N0 <= m ; :: thesis: y <= L . m

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

hence L is convergent ; :: thesis: integral' (M,g) <= lim L

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