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 st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

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 st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

let M be sigma_Measure of S; :: thesis: for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

let g be PartFunc of X,ExtREAL; :: thesis: for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( g is_simple_func_in S & g is nonnegative & ( 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) ) ) implies ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) )

assume that

A1: g is_simple_func_in S and

A2: g is nonnegative 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) ) ; :: thesis: ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

set E0 = eq_dom (g,0);

reconsider DG = dom g as Element of S by A1, Th37;

g is DG -measurable by A1, MESFUNC2:34;

then reconsider GG = DG /\ (great_eq_dom (g,0)) as Element of S by MESFUNC1:27;

for x being object st x in eq_dom (g,0) holds

x in dom g by MESFUNC1:def 15;

then A8: eq_dom (g,0) c= DG ;

then A9: DG = DG \/ (eq_dom (g,0)) by XBOOLE_1:12

.= (DG \ (eq_dom (g,0))) \/ (eq_dom (g,0)) by XBOOLE_1:39 ;

set E9 = (dom g) \ (eq_dom (g,0));

g is GG -measurable by A1, MESFUNC2:34;

then GG /\ (less_eq_dom (g,0)) in S by MESFUNC1:28;

then A10: DG /\ (eq_dom (g,0)) in S by MESFUNC1:18;

then eq_dom (g,0) in S by A8, XBOOLE_1:28;

then A11: X \ (eq_dom (g,0)) in S by MEASURE1:34;

DG /\ (X \ (eq_dom (g,0))) = (DG /\ X) \ (eq_dom (g,0)) by XBOOLE_1:49

.= DG \ (eq_dom (g,0)) by XBOOLE_1:28 ;

then reconsider E9 = (dom g) \ (eq_dom (g,0)) as Element of S by A11, MEASURE1:34;

reconsider E0 = eq_dom (g,0) as Element of S by A8, A10, XBOOLE_1:28;

A12: E0 misses E9 by XBOOLE_1:79;

thus ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) :: thesis: verum

for M being sigma_Measure of S

for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

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 st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

let M be sigma_Measure of S; :: thesis: for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

let g be PartFunc of X,ExtREAL; :: thesis: for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( 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) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( g is_simple_func_in S & g is nonnegative & ( 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) ) ) implies ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) )

assume that

A1: g is_simple_func_in S and

A2: g is nonnegative 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) ) ; :: thesis: ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

set E0 = eq_dom (g,0);

reconsider DG = dom g as Element of S by A1, Th37;

g is DG -measurable by A1, MESFUNC2:34;

then reconsider GG = DG /\ (great_eq_dom (g,0)) as Element of S by MESFUNC1:27;

for x being object st x in eq_dom (g,0) holds

x in dom g by MESFUNC1:def 15;

then A8: eq_dom (g,0) c= DG ;

then A9: DG = DG \/ (eq_dom (g,0)) by XBOOLE_1:12

.= (DG \ (eq_dom (g,0))) \/ (eq_dom (g,0)) by XBOOLE_1:39 ;

set E9 = (dom g) \ (eq_dom (g,0));

g is GG -measurable by A1, MESFUNC2:34;

then GG /\ (less_eq_dom (g,0)) in S by MESFUNC1:28;

then A10: DG /\ (eq_dom (g,0)) in S by MESFUNC1:18;

then eq_dom (g,0) in S by A8, XBOOLE_1:28;

then A11: X \ (eq_dom (g,0)) in S by MEASURE1:34;

DG /\ (X \ (eq_dom (g,0))) = (DG /\ X) \ (eq_dom (g,0)) by XBOOLE_1:49

.= DG \ (eq_dom (g,0)) by XBOOLE_1:28 ;

then reconsider E9 = (dom g) \ (eq_dom (g,0)) as Element of S by A11, MEASURE1:34;

reconsider E0 = eq_dom (g,0) as Element of S by A8, A10, XBOOLE_1:28;

A12: E0 misses E9 by XBOOLE_1:79;

thus ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) :: thesis: verum

proof

A13: dom (g | E9) =
(dom g) /\ E9
by RELAT_1:61

.= E9 by A9, XBOOLE_1:7, XBOOLE_1:28 ;

A14: for x being object st x in dom (g | E9) holds

0 < (g | E9) . x_{1}( Nat) -> Element of ExtREAL = integral' (M,((F . $1) | E9));

deffunc H_{2}( Nat) -> Element of ExtREAL = integral' (M,(F . $1));

deffunc H_{3}( Nat) -> Element of bool [:X,ExtREAL:] = (F . $1) | E9;

consider F9 being Functional_Sequence of X,ExtREAL such that

A17: for n being Nat holds F9 . n = H_{3}(n)
from SEQFUNC:sch 1();

consider L being ExtREAL_sequence such that

A18: for n being Element of NAT holds L . n = H_{1}(n)
from FUNCT_2:sch 4();

A21: for n being Element of NAT holds G . n = H_{2}(n)
from FUNCT_2:sch 4();

take G ; :: thesis: ( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

A22: for x being object st x in dom g holds

g . x = g . x ;

dom g = (E0 \/ E9) /\ (dom g) by A9;

then g | (E0 \/ E9) = g by A22, FUNCT_1:46;

then A23: integral' (M,g) = (integral' (M,(g | E0))) + (integral' (M,(g | E9))) by A1, A2, Th67, XBOOLE_1:79;

integral' (M,(g | E0)) = 0 by A1, A2, Th72;

then A24: integral' (M,g) = integral' (M,(g | E9)) by A23, XXREAL_3:4;

A25: g | E9 is_simple_func_in S by A1, Th34;

A26: for n being Nat holds

( (F . n) | E9 is_simple_func_in S & F9 . n is_simple_func_in S )

( dom ((F . n) | E9) = dom (g | E9) & dom (F9 . n) = dom (g | E9) )

( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) )

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

for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x )

for x being Element of X st x in dom (g | E9) holds

(F9 . n) . x <= (F9 . m) . x ;

then A41: integral' (M,(g | E9)) <= lim L by A25, A14, A27, A26, A29, A34, A20, Th74;

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

L . n <= L . m

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

G . n <= G . m

hence ( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) by A24, A55, A62, A41, A54, A61, Th54, XXREAL_0:2; :: thesis: verum

end;.= E9 by A9, XBOOLE_1:7, XBOOLE_1:28 ;

A14: for x being object st x in dom (g | E9) holds

0 < (g | E9) . x

proof

deffunc H
let x be object ; :: thesis: ( x in dom (g | E9) implies 0 < (g | E9) . x )

assume A15: x in dom (g | E9) ; :: thesis: 0 < (g | E9) . x

then A16: not x in E0 by A13, XBOOLE_0:def 5;

x in DG by A13, A15, XBOOLE_0:def 5;

then g . x <> 0 by A16, MESFUNC1:def 15;

then 0 < g . x by A2, SUPINF_2:51;

hence 0 < (g | E9) . x by A15, FUNCT_1:47; :: thesis: verum

end;assume A15: x in dom (g | E9) ; :: thesis: 0 < (g | E9) . x

then A16: not x in E0 by A13, XBOOLE_0:def 5;

x in DG by A13, A15, XBOOLE_0:def 5;

then g . x <> 0 by A16, MESFUNC1:def 15;

then 0 < g . x by A2, SUPINF_2:51;

hence 0 < (g | E9) . x by A15, FUNCT_1:47; :: thesis: verum

deffunc H

deffunc H

consider F9 being Functional_Sequence of X,ExtREAL such that

A17: for n being Nat holds F9 . n = H

consider L being ExtREAL_sequence such that

A18: for n being Element of NAT holds L . n = H

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

A20:
for n being Nat holds L . n = integral' (M,(F9 . n))
let n be Nat; :: thesis: L . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

hence L . n = H_{1}(n)
by A18; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence L . n = H

proof

consider G being ExtREAL_sequence such that
let n be Nat; :: thesis: L . n = integral' (M,(F9 . n))

thus L . n = integral' (M,((F . n) | E9)) by A19

.= integral' (M,(F9 . n)) by A17 ; :: thesis: verum

end;thus L . n = integral' (M,((F . n) | E9)) by A19

.= integral' (M,(F9 . n)) by A17 ; :: thesis: verum

A21: for n being Element of NAT holds G . n = H

take G ; :: thesis: ( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

A22: for x being object st x in dom g holds

g . x = g . x ;

dom g = (E0 \/ E9) /\ (dom g) by A9;

then g | (E0 \/ E9) = g by A22, FUNCT_1:46;

then A23: integral' (M,g) = (integral' (M,(g | E0))) + (integral' (M,(g | E9))) by A1, A2, Th67, XBOOLE_1:79;

integral' (M,(g | E0)) = 0 by A1, A2, Th72;

then A24: integral' (M,g) = integral' (M,(g | E9)) by A23, XXREAL_3:4;

A25: g | E9 is_simple_func_in S by A1, Th34;

A26: for n being Nat holds

( (F . n) | E9 is_simple_func_in S & F9 . n is_simple_func_in S )

proof

A27:
for n being Nat holds
let n be Nat; :: thesis: ( (F . n) | E9 is_simple_func_in S & F9 . n is_simple_func_in S )

thus (F . n) | E9 is_simple_func_in S by A3, Th34; :: thesis: F9 . n is_simple_func_in S

hence F9 . n is_simple_func_in S by A17; :: thesis: verum

end;thus (F . n) | E9 is_simple_func_in S by A3, Th34; :: thesis: F9 . n is_simple_func_in S

hence F9 . n is_simple_func_in S by A17; :: thesis: verum

( dom ((F . n) | E9) = dom (g | E9) & dom (F9 . n) = dom (g | E9) )

proof

A29:
for x being Element of X st x in dom (g | E9) holds
let n be Nat; :: thesis: ( dom ((F . n) | E9) = dom (g | E9) & dom (F9 . n) = dom (g | E9) )

A28: dom (F . n) = E9 \/ E0 by A4, A9;

thus dom ((F . n) | E9) = (dom (F . n)) /\ E9 by RELAT_1:61

.= dom (g | E9) by A13, A28, XBOOLE_1:7, XBOOLE_1:28 ; :: thesis: dom (F9 . n) = dom (g | E9)

hence dom (F9 . n) = dom (g | E9) by A17; :: thesis: verum

end;A28: dom (F . n) = E9 \/ E0 by A4, A9;

thus dom ((F . n) | E9) = (dom (F . n)) /\ E9 by RELAT_1:61

.= dom (g | E9) by A13, A28, XBOOLE_1:7, XBOOLE_1:28 ; :: thesis: dom (F9 . n) = dom (g | E9)

hence dom (F9 . n) = dom (g | E9) by A17; :: thesis: verum

( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) )

proof

A34:
for n being Nat holds F9 . n is nonnegative
let x be Element of X; :: thesis: ( x in dom (g | E9) implies ( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) ) )

assume A30: x in dom (g | E9) ; :: thesis: ( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) )

x in (dom g) /\ E9 by A30, RELAT_1:61;

then A33: x in dom g by XBOOLE_0:def 4;

then g . x <= lim (F # x) by A7;

hence ( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) ) by A7, A30, A33, A32, FUNCT_1:47; :: thesis: verum

end;assume A30: x in dom (g | E9) ; :: thesis: ( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) )

now :: thesis: for n being Element of NAT holds (F9 # x) . n = (F # x) . n

then A32:
F9 # x = F # x
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (F9 # x) . n = (F # x) . n

A31: x in dom ((F . n) | E9) by A27, A30;

thus (F9 # x) . n = (F9 . n) . x by Def13

.= ((F . n) | E9) . x by A17

.= (F . n) . x by A31, FUNCT_1:47

.= (F # x) . n by Def13 ; :: thesis: verum

end;A31: x in dom ((F . n) | E9) by A27, A30;

thus (F9 # x) . n = (F9 . n) . x by Def13

.= ((F . n) | E9) . x by A17

.= (F . n) . x by A31, FUNCT_1:47

.= (F # x) . n by Def13 ; :: thesis: verum

x in (dom g) /\ E9 by A30, RELAT_1:61;

then A33: x in dom g by XBOOLE_0:def 4;

then g . x <= lim (F # x) by A7;

hence ( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) ) by A7, A30, A33, A32, FUNCT_1:47; :: thesis: verum

proof

A35:
E9 c= dom g
by A9, XBOOLE_1:7;
let n be Nat; :: thesis: F9 . n is nonnegative

(F . n) | E9 is nonnegative by A5, Th15;

hence F9 . n is nonnegative by A17; :: thesis: verum

end;(F . n) | E9 is nonnegative by A5, Th15;

hence F9 . n is nonnegative by A17; :: thesis: verum

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

for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x )

proof

then
for n, m being Nat st n <= m holds
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x ) )

assume A37: n <= m ; :: thesis: for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x )

thus for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x ) :: thesis: verum

end;( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x ) )

assume A37: n <= m ; :: thesis: for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x )

thus for x being Element of X st x in dom (g | E9) holds

( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x ) :: thesis: verum

proof

let x be Element of X; :: thesis: ( x in dom (g | E9) implies ( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x ) )

assume A38: x in dom (g | E9) ; :: thesis: ( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x )

then A39: x in dom ((F . n) | E9) by A27;

(F . n) . x <= (F . m) . x by A6, A35, A13, A37, A38;

then A40: ((F . n) | E9) . x <= (F . m) . x by A39, FUNCT_1:47;

x in dom ((F . m) | E9) by A27, A38;

hence ((F . n) | E9) . x <= ((F . m) | E9) . x by A40, FUNCT_1:47; :: thesis: (F9 . n) . x <= (F9 . m) . x

then (F9 . n) . x <= ((F . m) | E9) . x by A17;

hence (F9 . n) . x <= (F9 . m) . x by A17; :: thesis: verum

end;assume A38: x in dom (g | E9) ; :: thesis: ( ((F . n) | E9) . x <= ((F . m) | E9) . x & (F9 . n) . x <= (F9 . m) . x )

then A39: x in dom ((F . n) | E9) by A27;

(F . n) . x <= (F . m) . x by A6, A35, A13, A37, A38;

then A40: ((F . n) | E9) . x <= (F . m) . x by A39, FUNCT_1:47;

x in dom ((F . m) | E9) by A27, A38;

hence ((F . n) | E9) . x <= ((F . m) | E9) . x by A40, FUNCT_1:47; :: thesis: (F9 . n) . x <= (F9 . m) . x

then (F9 . n) . x <= ((F . m) | E9) . x by A17;

hence (F9 . n) . x <= (F9 . m) . x by A17; :: thesis: verum

for x being Element of X st x in dom (g | E9) holds

(F9 . n) . x <= (F9 . m) . x ;

then A41: integral' (M,(g | E9)) <= lim L by A25, A14, A27, A26, A29, A34, A20, Th74;

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

L . n <= L . m

proof

then A54:
lim L = sup (rng L)
by Th54;
let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )

A42: F9 . m is_simple_func_in S by A26;

A43: dom (F9 . m) = dom (g | E9) by A27;

A44: L . m = integral' (M,(F9 . m)) by A20;

A45: L . n = integral' (M,(F9 . n)) by A20;

A46: dom (F9 . n) = dom (g | E9) by A27;

assume A47: n <= m ; :: thesis: L . n <= L . m

A48: for x being object st x in dom ((F9 . m) - (F9 . n)) holds

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

A50: F9 . n is nonnegative by A34;

A51: F9 . n is_simple_func_in S by A26;

then A52: dom ((F9 . m) - (F9 . n)) = (dom (F9 . m)) /\ (dom (F9 . n)) by A42, A50, A49, A48, Th69;

then A53: (F9 . m) | (dom ((F9 . m) - (F9 . n))) = F9 . m by A46, A43, GRFUNC_1:23;

(F9 . n) | (dom ((F9 . m) - (F9 . n))) = F9 . n by A46, A43, A52, GRFUNC_1:23;

hence L . n <= L . m by A51, A42, A50, A49, A48, A53, A45, A44, Th70; :: thesis: verum

end;A42: F9 . m is_simple_func_in S by A26;

A43: dom (F9 . m) = dom (g | E9) by A27;

A44: L . m = integral' (M,(F9 . m)) by A20;

A45: L . n = integral' (M,(F9 . n)) by A20;

A46: dom (F9 . n) = dom (g | E9) by A27;

assume A47: n <= m ; :: thesis: L . n <= L . m

A48: for x being object st x in dom ((F9 . m) - (F9 . n)) holds

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

proof

A49:
F9 . m is nonnegative
by A34;
let x be object ; :: thesis: ( x in dom ((F9 . m) - (F9 . n)) implies (F9 . n) . x <= (F9 . m) . x )

assume x in dom ((F9 . m) - (F9 . n)) ; :: thesis: (F9 . n) . x <= (F9 . m) . x

then x in ((dom (F9 . m)) /\ (dom (F9 . n))) \ ((((F9 . m) " {+infty}) /\ ((F9 . n) " {+infty})) \/ (((F9 . m) " {-infty}) /\ ((F9 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F9 . m)) /\ (dom (F9 . n)) by XBOOLE_0:def 5;

hence (F9 . n) . x <= (F9 . m) . x by A36, A47, A46, A43; :: thesis: verum

end;assume x in dom ((F9 . m) - (F9 . n)) ; :: thesis: (F9 . n) . x <= (F9 . m) . x

then x in ((dom (F9 . m)) /\ (dom (F9 . n))) \ ((((F9 . m) " {+infty}) /\ ((F9 . n) " {+infty})) \/ (((F9 . m) " {-infty}) /\ ((F9 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F9 . m)) /\ (dom (F9 . n)) by XBOOLE_0:def 5;

hence (F9 . n) . x <= (F9 . m) . x by A36, A47, A46, A43; :: thesis: verum

A50: F9 . n is nonnegative by A34;

A51: F9 . n is_simple_func_in S by A26;

then A52: dom ((F9 . m) - (F9 . n)) = (dom (F9 . m)) /\ (dom (F9 . n)) by A42, A50, A49, A48, Th69;

then A53: (F9 . m) | (dom ((F9 . m) - (F9 . n))) = F9 . m by A46, A43, GRFUNC_1:23;

(F9 . n) | (dom ((F9 . m) - (F9 . n))) = F9 . n by A46, A43, A52, GRFUNC_1:23;

hence L . n <= L . m by A51, A42, A50, A49, A48, A53, A45, A44, Th70; :: thesis: verum

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

for n being Nat holds L . n <= G . n
let n be Nat; :: thesis: G . n = H_{2}(n)

n in NAT by ORDINAL1:def 12;

hence G . n = H_{2}(n)
by A21; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence G . n = H

proof

then A61:
sup (rng L) <= sup (rng G)
by Th55;
let n be Nat; :: thesis: L . n <= G . n

A56: F . n is_simple_func_in S by A3;

dom (F . n) = E9 \/ E0 by A4, A9;

then A57: dom (F . n) = (E0 \/ E9) /\ (dom (F . n)) ;

for x being object st x in dom (F . n) holds

(F . n) . x = (F . n) . x ;

then A58: F . n = (F . n) | (E0 \/ E9) by A57, FUNCT_1:46;

then (F . n) | (E0 \/ E9) is nonnegative by A5;

then A59: integral' (M,(F . n)) = (integral' (M,((F . n) | E0))) + (integral' (M,((F . n) | E9))) by A3, A12, A58, Th67;

(F . n) | E0 is nonnegative by A5, Th15;

then 0 <= integral' (M,((F . n) | E0)) by A56, Th34, Th68;

then A60: integral' (M,((F . n) | E9)) <= integral' (M,(F . n)) by A59, XXREAL_3:39;

G . n = integral' (M,(F . n)) by A55;

hence L . n <= G . n by A19, A60; :: thesis: verum

end;A56: F . n is_simple_func_in S by A3;

dom (F . n) = E9 \/ E0 by A4, A9;

then A57: dom (F . n) = (E0 \/ E9) /\ (dom (F . n)) ;

for x being object st x in dom (F . n) holds

(F . n) . x = (F . n) . x ;

then A58: F . n = (F . n) | (E0 \/ E9) by A57, FUNCT_1:46;

then (F . n) | (E0 \/ E9) is nonnegative by A5;

then A59: integral' (M,(F . n)) = (integral' (M,((F . n) | E0))) + (integral' (M,((F . n) | E9))) by A3, A12, A58, Th67;

(F . n) | E0 is nonnegative by A5, Th15;

then 0 <= integral' (M,((F . n) | E0)) by A56, Th34, Th68;

then A60: integral' (M,((F . n) | E9)) <= integral' (M,(F . n)) by A59, XXREAL_3:39;

G . n = integral' (M,(F . n)) by A55;

hence L . n <= G . n by A19, A60; :: thesis: verum

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

G . n <= G . m

proof

then
lim G = sup (rng G)
by Th54;
let n, m be Nat; :: thesis: ( n <= m implies G . n <= G . m )

A63: F . m is_simple_func_in S by A3;

A64: dom (F . m) = dom g by A4;

A65: G . m = integral' (M,(F . m)) by A55;

A66: G . n = integral' (M,(F . n)) by A55;

A67: dom (F . n) = dom g by A4;

assume A68: n <= m ; :: thesis: G . n <= G . m

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

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

A71: F . n is nonnegative by A5;

A72: F . n is_simple_func_in S by A3;

then A73: dom ((F . m) - (F . n)) = (dom (F . m)) /\ (dom (F . n)) by A63, A71, A70, A69, Th69;

then A74: (F . m) | (dom ((F . m) - (F . n))) = F . m by A67, A64, GRFUNC_1:23;

(F . n) | (dom ((F . m) - (F . n))) = F . n by A67, A64, A73, GRFUNC_1:23;

hence G . n <= G . m by A72, A63, A71, A70, A69, A74, A66, A65, Th70; :: thesis: verum

end;A63: F . m is_simple_func_in S by A3;

A64: dom (F . m) = dom g by A4;

A65: G . m = integral' (M,(F . m)) by A55;

A66: G . n = integral' (M,(F . n)) by A55;

A67: dom (F . n) = dom g by A4;

assume A68: n <= m ; :: thesis: G . n <= G . m

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

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

proof

A70:
F . m is nonnegative
by A5;
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, A68, A67, A64; :: 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, A68, A67, A64; :: thesis: verum

A71: F . n is nonnegative by A5;

A72: F . n is_simple_func_in S by A3;

then A73: dom ((F . m) - (F . n)) = (dom (F . m)) /\ (dom (F . n)) by A63, A71, A70, A69, Th69;

then A74: (F . m) | (dom ((F . m) - (F . n))) = F . m by A67, A64, GRFUNC_1:23;

(F . n) | (dom ((F . m) - (F . n))) = F . n by A67, A64, A73, GRFUNC_1:23;

hence G . n <= G . m by A72, A63, A71, A70, A69, A74, A66, A65, Th70; :: thesis: verum

hence ( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) by A24, A55, A62, A41, A54, A61, Th54, XXREAL_0:2; :: thesis: verum