proof

A13: dom (g | E9) = (dom g) /\ E9 by RELAT_1:90
.= E9 by A9, XBOOLE_1:7, XBOOLE_1:28 ;
A14: for x being set st x in dom (g | E9) holds
0 < (g | E9) . x

proof

let x be set ; :: thesis:
assume A15: x in dom (g | E9) ; :: thesis:
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 16;
then 0 < g . x by A2, SUPINF_2:70;
hence 0 < (g | E9) . x by A15, FUNCT_1:70; :: thesis:

end;

deffunc H₁( Nat) -> Element of ExtREAL = integral' M,((F . $1) | E9);
deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(F . $1);
deffunc H₃( 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₃(n) from SEQFUNC:sch 1();
consider L being ExtREAL_sequence such that
A18: for n being Element of NAT holds L . n = H₁(n) from FUNCT_2:sch 4();

A19: now

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

end;

A20: for n being Nat holds L . n = integral' M,(F9 . n)

proof

let n be Nat; :: thesis:
thus L . n = integral' M,((F . n) | E9) by A19
.= integral' M,(F9 . n) by A17 ; :: thesis:

end;

consider G being ExtREAL_sequence such that
A21: for n being Element of NAT holds G . n = H₂(n) from FUNCT_2:sch 4();
take G ; :: thesis:
A22: for x being set 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:68;
then A23: integral' M,g = (integral' M,(g | E0)) + (integral' M,(g | E9)) by A1, A2, Th73, XBOOLE_1:79;
integral' M,(g | E0) = 0 by A1, A2, Th78;
then A24: integral' M,g = integral' M,(g | E9) by A23, XXREAL_3:4;
A25: g | E9 is_simple_func_in S by A1, Th40;
A26: for n being Nat holds
( (F . n) | E9 is_simple_func_in S & F9 . n is_simple_func_in S )

proof

let n be Nat; :: thesis:
thus (F . n) | E9 is_simple_func_in S by A3, Th40; :: thesis:
hence F9 . n is_simple_func_in S by A17; :: thesis:

end;

A27: for n being Nat holds
( dom ((F . n) | E9) = dom (g | E9) & dom (F9 . n) = dom (g | E9) )

proof

let n be Nat; :: thesis:
A28: dom (F . n) = E9 \/ E0 by A4, A9;
thus dom ((F . n) | E9) = (dom (F . n)) /\ E9 by RELAT_1:90
.= dom (g | E9) by A13, A28, XBOOLE_1:7, XBOOLE_1:28 ; :: thesis:
hence dom (F9 . n) = dom (g | E9) by A17; :: thesis:

end;

A29: for x being Element of X st x in dom (g | E9) holds
( F9 # x is convergent & (g | E9) . x <= lim (F9 # x) )

proof

let x be Element of X; :: thesis:
assume A30: x in dom (g | E9) ; :: thesis:

now

let n be Element of NAT ; :: thesis:
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:70
.= (F # x) . n by Def13 ; :: thesis:

end;

then A32: F9 # x = F # x by FUNCT_2:113;
x in (dom g) /\ E9 by A30, RELAT_1:90;
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:70; :: thesis:

end;

A34: for n being Nat holds F9 . n is nonnegative

proof

let n be Nat; :: thesis:
(F . n) | E9 is nonnegative by A5, Th21;
hence F9 . n is nonnegative by A17; :: thesis:

end;

A35: E9 c= dom g by A9, XBOOLE_1:7;
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

let n, m be Nat; :: thesis:
assume A37: n <= m ; :: thesis:
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:

proof

let x be Element of X; :: thesis:
assume A38: x in dom (g | E9) ; :: thesis:
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:70;
x in dom ((F . m) | E9) by A27, A38;
hence ((F . n) | E9) . x <= ((F . m) | E9) . x by A40, FUNCT_1:70; :: thesis:
then (F9 . n) . x <= ((F . m) | E9) . x by A17;
hence (F9 . n) . x <= (F9 . m) . x by A17; :: thesis:

end;

then for n, m being Nat st n <= m holds
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, Th80;
for n, m being Nat st n <= m holds
L . n <= L . m

proof

let n, m be Nat; :: thesis:
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:
A48: for x being set st x in dom ((F9 . m) - (F9 . n)) holds
(F9 . n) . x <= (F9 . m) . x

proof

let x be set ; :: thesis:
assume x in dom ((F9 . m) - (F9 . n)) ; :: thesis:
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:

end;

A49: F9 . m is nonnegative by A34;
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, Th75;
then A53: (F9 . m) | (dom ((F9 . m) - (F9 . n))) = F9 . m by A46, A43, GRFUNC_1:64;
(F9 . n) | (dom ((F9 . m) - (F9 . n))) = F9 . n by A46, A43, A52, GRFUNC_1:64;
hence L . n <= L . m by A51, A42, A50, A49, A48, A53, A45, A44, Th76; :: thesis:

end;

then A54: lim L = sup (rng L) by Th60;

A55: now

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

end;

for n being Nat holds L . n <= G . n

proof

let n be Nat; :: thesis:
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 set 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:68;
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, Th73;
(F . n) | E0 is nonnegative by A5, Th21;
then 0 <= integral' M,((F . n) | E0) by A56, Th40, Th74;
then A60: integral' M,((F . n) | E9) <= integral' M,(F . n) by A59, XXREAL_3:42;
G . n = integral' M,(F . n) by A55;
hence L . n <= G . n by A19, A60; :: thesis:

end;

then A61: sup (rng L) <= sup (rng G) by Th61;
A62: for n, m being Nat st n <= m holds
G . n <= G . m

proof

let n, m be Nat; :: thesis:
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:
A69: for x being set st x in dom ((F . m) - (F . n)) holds
(F . n) . x <= (F . m) . x

proof

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

end;

A70: F . m is nonnegative by A5;
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, Th75;
then A74: (F . m) | (dom ((F . m) - (F . n))) = F . m by A67, A64, GRFUNC_1:64;
(F . n) | (dom ((F . m) - (F . n))) = F . n by A67, A64, A73, GRFUNC_1:64;
hence G . n <= G . m by A72, A63, A71, A70, A69, A74, A66, A65, Th76; :: thesis:

end;

then lim G = sup (rng G) by Th60;
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, Th60, XXREAL_0:2; :: thesis:

end;