let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let g be PartFunc of X,ExtREAL; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
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:
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:

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

proof

let x be object ; :: 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 15;
then 0 < g . x by A2, SUPINF_2:51;
hence 0 < (g | E9) . x by A15, FUNCT_1:47; :: 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 :: thesis:

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

let n be Nat; :: thesis:
thus (F . n) | E9 is_simple_func_in S by A3, Th34; :: 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:61
.= 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 :: thesis:

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:47
.= (F # x) . n by Def13 ; :: thesis:

end;

then A32: F9 # x = F # x by FUNCT_2:63;
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:

end;

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

proof

let n be Nat; :: thesis:
(F . n) | E9 is nonnegative by A5, Th15;
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: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:
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, Th74;
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 object st x in dom ((F9 . m) - (F9 . n)) holds
(F9 . n) . x <= (F9 . m) . x

proof

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

end;

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

A55: now :: thesis:

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

end;

then A61: sup (rng L) <= sup (rng G) by Th55;
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 object st x in dom ((F . m) - (F . n)) holds
(F . n) . x <= (F . m) . x

proof

let x be object ; :: thesis:
assume x in dom ((F . m) - (F . n)) ; :: thesis:
then x in ((dom (F . m)) /\ (dom (F . n))) \ ((((F . m) " {+infty}) /\ ((F . n) " {+infty})) \/ (((F . m) " {-infty}) /\ ((F . n) " {-infty}))) by MESFUNC1:def 4;
then x in (dom (F . m)) /\ (dom (F . n)) by XBOOLE_0:def 5;
hence (F . n) . x <= (F . m) . x by A6, 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, 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:

end;

then lim G = sup (rng G) by Th54;
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:

end;