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 )
reconsider DG = dom g as Element of S by A1, Th43;
set E0 = eq_dom g,(R_EAL 0 );
set E' = (dom g) \ (eq_dom g,(R_EAL 0 ));
for x being set st x in eq_dom g,(R_EAL 0 ) holds
x in dom g by MESFUNC1:def 16;
then A8: eq_dom g,(R_EAL 0 ) c= DG by TARSKI:def 3;
then A9: DG = DG \/ (eq_dom g,(R_EAL 0 )) by XBOOLE_1:12
.= (DG \ (eq_dom g,(R_EAL 0 ))) \/ (eq_dom g,(R_EAL 0 )) by XBOOLE_1:39 ;
g is_measurable_on DG by A1, MESFUNC2:37;
then reconsider GG = DG /\ (great_eq_dom g,(R_EAL 0 )) as Element of S by MESFUNC1:31;
g is_measurable_on GG by A1, MESFUNC2:37;
then GG /\ (less_eq_dom g,(R_EAL 0 )) in S by MESFUNC1:32;
then A10: DG /\ (eq_dom g,(R_EAL 0 )) in S by MESFUNC1:22;
then eq_dom g,(R_EAL 0 ) in S by A8, XBOOLE_1:28;
then A11: X \ (eq_dom g,(R_EAL 0 )) in S by MEASURE1:66;
DG /\ (X \ (eq_dom g,(R_EAL 0 ))) = (DG /\ X) \ (eq_dom g,(R_EAL 0 )) by XBOOLE_1:49
.= DG \ (eq_dom g,(R_EAL 0 )) by XBOOLE_1:28 ;
then reconsider E' = (dom g) \ (eq_dom g,(R_EAL 0 )) as Element of S by A11, MEASURE1:66;
reconsider E0 = eq_dom g,(R_EAL 0 ) as Element of S by A8, A10, XBOOLE_1:28;
A13: E0 misses E' 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

A14: E' c= dom g by A9, XBOOLE_1:7;
A15: dom (g | E') = (dom g) /\ E' by RELAT_1:90
.= E' by A9, XBOOLE_1:7, XBOOLE_1:28 ;
A16: g | E' is_simple_func_in S by A1, Th40;
A17: for x being set st x in dom (g | E') holds
0 < (g | E') . x

proof

let x be set ; :: thesis: ( x in dom (g | E') implies 0 < (g | E') . x )
assume A18: x in dom (g | E') ; :: thesis: 0 < (g | E') . x
then ( x in DG & not x in E0 ) by A15, XBOOLE_0:def 5;
then g . x <> 0 by MESFUNC1:def 16;
then 0 < g . x by A2, SUPINF_2:70;
hence 0 < (g | E') . x by A18, FUNCT_1:70; :: thesis: verum

end;

deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F . $1) | E';
consider F' being Functional_Sequence of X,ExtREAL such that
A19: for n being Nat holds F' . n = H₁(n) from SEQFUNC:sch 1();
A20: for n being Nat holds
( dom ((F . n) | E') = dom (g | E') & dom (F' . n) = dom (g | E') )

proof

let n be Nat; :: thesis: ( dom ((F . n) | E') = dom (g | E') & dom (F' . n) = dom (g | E') )
A21: dom (F . n) = E' \/ E0 by A4, A9;
thus dom ((F . n) | E') = (dom (F . n)) /\ E' by RELAT_1:90
.= dom (g | E') by A15, A21, XBOOLE_1:7, XBOOLE_1:28 ; :: thesis: dom (F' . n) = dom (g | E')
hence dom (F' . n) = dom (g | E') by A19; :: thesis: verum

end;

A22: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (g | E') holds
( ((F . n) | E') . x <= ((F . m) | E') . x & (F' . n) . x <= (F' . m) . x )

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom (g | E') holds
( ((F . n) | E') . x <= ((F . m) | E') . x & (F' . n) . x <= (F' . m) . x ) )
assume A23: n <= m ; :: thesis: for x being Element of X st x in dom (g | E') holds
( ((F . n) | E') . x <= ((F . m) | E') . x & (F' . n) . x <= (F' . m) . x )
thus for x being Element of X st x in dom (g | E') holds
( ((F . n) | E') . x <= ((F . m) | E') . x & (F' . n) . x <= (F' . m) . x ) :: thesis: verum

proof

let x be Element of X; :: thesis: ( x in dom (g | E') implies ( ((F . n) | E') . x <= ((F . m) | E') . x & (F' . n) . x <= (F' . m) . x ) )
assume A24: x in dom (g | E') ; :: thesis: ( ((F . n) | E') . x <= ((F . m) | E') . x & (F' . n) . x <= (F' . m) . x )
then A25: ( x in dom ((F . m) | E') & x in dom ((F . n) | E') ) by A20;
(F . n) . x <= (F . m) . x by A6, A14, A15, A23, A24;
then ((F . n) | E') . x <= (F . m) . x by A25, FUNCT_1:70;
hence ((F . n) | E') . x <= ((F . m) | E') . x by A25, FUNCT_1:70; :: thesis: (F' . n) . x <= (F' . m) . x
then (F' . n) . x <= ((F . m) | E') . x by A19;
hence (F' . n) . x <= (F' . m) . x by A19; :: thesis: verum

end;

end;

A26: for n being Nat holds
( (F . n) | E' is_simple_func_in S & F' . n is_simple_func_in S )

proof

let n be Nat; :: thesis: ( (F . n) | E' is_simple_func_in S & F' . n is_simple_func_in S )
thus (F . n) | E' is_simple_func_in S by A3, Th40; :: thesis: F' . n is_simple_func_in S
hence F' . n is_simple_func_in S by A19; :: thesis: verum

end;

A27: for x being Element of X st x in dom (g | E') holds
( F' # x is convergent & (g | E') . x <= lim (F' # x) )

proof

let x be Element of X; :: thesis: ( x in dom (g | E') implies ( F' # x is convergent & (g | E') . x <= lim (F' # x) ) )
assume A28: x in dom (g | E') ; :: thesis: ( F' # x is convergent & (g | E') . x <= lim (F' # x) )
then x in (dom g) /\ E' by RELAT_1:90;
then A29: x in dom g by XBOOLE_0:def 4;
A30: F' # x = F # x

proof

now

let n be Element of NAT ; :: thesis: (F' # x) . n = (F # x) . n
A31: x in dom ((F . n) | E') by A20, A28;
thus (F' # x) . n = (F' . n) . x by Def13
.= ((F . n) | E') . x by A19
.= (F . n) . x by A31, FUNCT_1:70
.= (F # x) . n by Def13 ; :: thesis: verum

end;

hence F' # x = F # x by FUNCT_2:113; :: thesis: verum

end;

( F # x is convergent & g . x <= lim (F # x) ) by A7, A29;
hence ( F' # x is convergent & (g | E') . x <= lim (F' # x) ) by A28, A30, FUNCT_1:70; :: thesis: verum

end;

A32: dom g = (E0 \/ E') /\ (dom g) by A9;
for x being set st x in dom g holds
g . x = g . x ;
then g | (E0 \/ E') = g by A32, FUNCT_1:68;
then A33: integral' M,g = (integral' M,(g | E0)) + (integral' M,(g | E')) by A1, A2, Th73, XBOOLE_1:79;
integral' M,(g | E0) = 0 by A1, A2, Th78;
then A34: integral' M,g = integral' M,(g | E') by A33, XXREAL_3:4;
deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(F . $1);
consider G being ExtREAL_sequence such that
A35: for n being Element of NAT holds G . n = H₂(n) from FUNCT_2:sch 4();

A36: now

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

end;

A37: for n, m being Nat st n <= m holds
G . n <= G . m

proof

let n, m be Nat; :: thesis: ( n <= m implies G . n <= G . m )
assume A38: n <= m ; :: thesis: G . n <= G . m
A39: ( F . n is_simple_func_in S & F . m is_simple_func_in S ) by A3;
A40: ( dom (F . n) = dom g & dom (F . m) = dom g ) by A4;
A41: ( F . n is nonnegative & F . m is nonnegative ) by A5;
A42: for x being set st x in dom ((F . m) - (F . n)) holds
(F . n) . x <= (F . m) . x

proof

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

end;

then dom ((F . m) - (F . n)) = (dom (F . m)) /\ (dom (F . n)) by A39, A41, Th75;
then A43: ( (F . n) | (dom ((F . m) - (F . n))) = F . n & (F . m) | (dom ((F . m) - (F . n))) = F . m ) by A40, GRFUNC_1:64;
( G . n = integral' M,(F . n) & G . m = integral' M,(F . m) ) by A36;
hence G . n <= G . m by A39, A41, A42, A43, Th76; :: thesis: verum

end;

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 )
A44: ( G is convergent & lim G = sup (rng G) ) by A37, Th60;
A45: for n being Nat holds F' . n is nonnegative

proof

let n be Nat; :: thesis: F' . n is nonnegative
(F . n) | E' is nonnegative by A5, Th21;
hence F' . n is nonnegative by A19; :: thesis: verum

end;

deffunc H₃( Nat) -> Element of ExtREAL = integral' M,((F . $1) | E');
consider L being ExtREAL_sequence such that
A46: for n being Element of NAT holds L . n = H₃(n) from FUNCT_2:sch 4();

A47: now

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

end;

A48: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (g | E') holds
(F' . n) . x <= (F' . m) . x by A22;
A49: for n being Nat holds L . n = integral' M,(F' . n)

proof

let n be Nat; :: thesis: L . n = integral' M,(F' . n)
thus L . n = integral' M,((F . n) | E') by A47
.= integral' M,(F' . n) by A19 ; :: thesis: verum

end;

then A50: ( L is convergent & integral' M,(g | E') <= lim L ) by A16, A17, A20, A26, A27, A45, A48, Th80;
for n, m being Nat st n <= m holds
L . n <= L . m

proof

let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )
assume A51: n <= m ; :: thesis: L . n <= L . m
A52: ( F' . n is_simple_func_in S & F' . m is_simple_func_in S ) by A26;
A53: ( dom (F' . n) = dom (g | E') & dom (F' . m) = dom (g | E') ) by A20;
A54: ( F' . n is nonnegative & F' . m is nonnegative ) by A45;
A55: for x being set st x in dom ((F' . m) - (F' . n)) holds
(F' . n) . x <= (F' . m) . x

proof

let x be set ; :: thesis: ( x in dom ((F' . m) - (F' . n)) implies (F' . n) . x <= (F' . m) . x )
assume x in dom ((F' . m) - (F' . n)) ; :: thesis: (F' . n) . x <= (F' . m) . x
then x in ((dom (F' . m)) /\ (dom (F' . n))) \ ((((F' . m) " {+infty }) /\ ((F' . n) " {+infty })) \/ (((F' . m) " {-infty }) /\ ((F' . n) " {-infty }))) by MESFUNC1:def 4;
then x in (dom (F' . m)) /\ (dom (F' . n)) by XBOOLE_0:def 5;
hence (F' . n) . x <= (F' . m) . x by A22, A51, A53; :: thesis: verum

end;

then dom ((F' . m) - (F' . n)) = (dom (F' . m)) /\ (dom (F' . n)) by A52, A54, Th75;
then A56: ( (F' . n) | (dom ((F' . m) - (F' . n))) = F' . n & (F' . m) | (dom ((F' . m) - (F' . n))) = F' . m ) by A53, GRFUNC_1:64;
( L . n = integral' M,(F' . n) & L . m = integral' M,(F' . m) ) by A49;
hence L . n <= L . m by A52, A54, A55, A56, Th76; :: thesis: verum

end;

then A57: ( L is convergent & lim L = sup (rng L) ) by Th60;
for n being Nat holds L . n <= G . n

proof

let n be Nat; :: thesis: L . n <= G . n
A58: G . n = integral' M,(F . n) by A36;
A59: dom (F . n) = E' \/ E0 by A4, A9;
A60: F . n is_simple_func_in S by A3;
( (F . n) | E0 is nonnegative & (F . n) | E' is nonnegative ) by A5, Th21;
then A61: ( 0 <= integral' M,((F . n) | E0) & 0 <= integral' M,((F . n) | E') ) by A60, Th40, Th74;
A62: dom (F . n) = (E0 \/ E') /\ (dom (F . n)) by A59;
for x being set st x in dom (F . n) holds
(F . n) . x = (F . n) . x ;
then A63: F . n = (F . n) | (E0 \/ E') by A62, FUNCT_1:68;
then (F . n) | (E0 \/ E') is nonnegative by A5;
then integral' M,(F . n) = (integral' M,((F . n) | E0)) + (integral' M,((F . n) | E')) by A3, A13, A63, Th73;
then integral' M,((F . n) | E') <= integral' M,(F . n) by A61, XXREAL_3:42;
hence L . n <= G . n by A47, A58; :: thesis: verum

end;

then sup (rng L) <= sup (rng G) by Th61;
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 A34, A36, A44, A50, A57, XXREAL_0:2; :: thesis: verum

end;