let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M implies ( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 ) )

A1: max+ f is nonnegative by Lm1;

assume A2: f is_integrable_on M ; :: thesis: ( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

then A3: integral+ (M,(max+ f)) < +infty ;

consider A being Element of S such that

A4: A = dom f and

A5: f is A -measurable by A2;

A6: for x being object holds

( ( x in eq_dom (f,+infty) implies x in A ) & ( x in eq_dom (f,-infty) implies x in A ) ) by A4, MESFUNC1:def 15;

then A7: eq_dom (f,+infty) c= A ;

then A8: A /\ (eq_dom (f,+infty)) = eq_dom (f,+infty) by XBOOLE_1:28;

A9: eq_dom (f,-infty) c= A by A6;

then A10: A /\ (eq_dom (f,-infty)) = eq_dom (f,-infty) by XBOOLE_1:28;

A11: A /\ (eq_dom (f,+infty)) in S by A4, A5, MESFUNC1:33;

then A12: f " {+infty} in S by A8, Th30;

A13: A /\ (eq_dom (f,-infty)) in S by A5, MESFUNC1:34;

then reconsider B2 = f " {-infty} as Element of S by A10, Th30;

A14: f " {-infty} in S by A13, A10, Th30;

thus ( f " {+infty} in S & f " {-infty} in S ) by A11, A13, A8, A10, Th30; :: thesis: ( M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

set C2 = A \ B2;

A15: integral+ (M,(max- f)) < +infty by A2;

reconsider B1 = f " {+infty} as Element of S by A11, A8, Th30;

A16: A = dom (max+ f) by A4, MESFUNC2:def 2;

then A17: B1 c= dom (max+ f) by A7, Th30;

then A18: B1 = (dom (max+ f)) /\ B1 by XBOOLE_1:28;

A19: max+ f is A -measurable by A5, MESFUNC2:25;

then max+ f is B1 -measurable by A16, A17, MESFUNC1:30;

then A20: (max+ f) | B1 is B1 -measurable by A18, Th42;

set C1 = A \ B1;

A21: for x being Element of X holds

( ( x in dom ((max+ f) | (B1 \/ (A \ B1))) implies ((max+ f) | (B1 \/ (A \ B1))) . x = (max+ f) . x ) & ( x in dom ((max- f) | (B2 \/ (A \ B2))) implies ((max- f) | (B2 \/ (A \ B2))) . x = (max- f) . x ) ) by FUNCT_1:47;

B1 \/ (A \ B1) = A by A16, A17, XBOOLE_1:45;

then dom ((max+ f) | (B1 \/ (A \ B1))) = (dom (max+ f)) /\ (dom (max+ f)) by A16, RELAT_1:61;

then (max+ f) | (B1 \/ (A \ B1)) = max+ f by A21, PARTFUN1:5;

then integral+ (M,(max+ f)) = (integral+ (M,((max+ f) | B1))) + (integral+ (M,((max+ f) | (A \ B1)))) by A1, A16, A19, Th81, XBOOLE_1:106;

then A22: integral+ (M,((max+ f) | B1)) <= integral+ (M,(max+ f)) by A1, A16, A19, Th80, XXREAL_3:65;

A47: max- f is nonnegative by Lm1;

A48: A = dom (max- f) by A4, MESFUNC2:def 3;

then A49: B2 c= dom (max- f) by A9, Th30;

then A50: B2 = (dom (max- f)) /\ B2 by XBOOLE_1:28;

A51: max- f is A -measurable by A4, A5, MESFUNC2:26;

then max- f is B2 -measurable by A48, A49, MESFUNC1:30;

then A52: (max- f) | B2 is B2 -measurable by A50, Th42;

B2 \/ (A \ B2) = A by A48, A49, XBOOLE_1:45;

then dom ((max- f) | (B2 \/ (A \ B2))) = (dom (max- f)) /\ (dom (max- f)) by A48, RELAT_1:61;

then (max- f) | (B2 \/ (A \ B2)) = max- f by A21, PARTFUN1:5;

then integral+ (M,(max- f)) = (integral+ (M,((max- f) | B2))) + (integral+ (M,((max- f) | (A \ B2)))) by A47, A48, A51, Th81, XBOOLE_1:106;

then A53: integral+ (M,((max- f) | B2)) <= integral+ (M,(max- f)) by A47, A48, A51, Th80, XXREAL_3:65;

thus M . ((f " {+infty}) \/ (f " {-infty})) = M . (B1 \/ B2)

.= 0 by A54, MEASURE1:38 ; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M implies ( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 ) )

A1: max+ f is nonnegative by Lm1;

assume A2: f is_integrable_on M ; :: thesis: ( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

then A3: integral+ (M,(max+ f)) < +infty ;

consider A being Element of S such that

A4: A = dom f and

A5: f is A -measurable by A2;

A6: for x being object holds

( ( x in eq_dom (f,+infty) implies x in A ) & ( x in eq_dom (f,-infty) implies x in A ) ) by A4, MESFUNC1:def 15;

then A7: eq_dom (f,+infty) c= A ;

then A8: A /\ (eq_dom (f,+infty)) = eq_dom (f,+infty) by XBOOLE_1:28;

A9: eq_dom (f,-infty) c= A by A6;

then A10: A /\ (eq_dom (f,-infty)) = eq_dom (f,-infty) by XBOOLE_1:28;

A11: A /\ (eq_dom (f,+infty)) in S by A4, A5, MESFUNC1:33;

then A12: f " {+infty} in S by A8, Th30;

A13: A /\ (eq_dom (f,-infty)) in S by A5, MESFUNC1:34;

then reconsider B2 = f " {-infty} as Element of S by A10, Th30;

A14: f " {-infty} in S by A13, A10, Th30;

thus ( f " {+infty} in S & f " {-infty} in S ) by A11, A13, A8, A10, Th30; :: thesis: ( M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

set C2 = A \ B2;

A15: integral+ (M,(max- f)) < +infty by A2;

reconsider B1 = f " {+infty} as Element of S by A11, A8, Th30;

A16: A = dom (max+ f) by A4, MESFUNC2:def 2;

then A17: B1 c= dom (max+ f) by A7, Th30;

then A18: B1 = (dom (max+ f)) /\ B1 by XBOOLE_1:28;

A19: max+ f is A -measurable by A5, MESFUNC2:25;

then max+ f is B1 -measurable by A16, A17, MESFUNC1:30;

then A20: (max+ f) | B1 is B1 -measurable by A18, Th42;

set C1 = A \ B1;

A21: for x being Element of X holds

( ( x in dom ((max+ f) | (B1 \/ (A \ B1))) implies ((max+ f) | (B1 \/ (A \ B1))) . x = (max+ f) . x ) & ( x in dom ((max- f) | (B2 \/ (A \ B2))) implies ((max- f) | (B2 \/ (A \ B2))) . x = (max- f) . x ) ) by FUNCT_1:47;

B1 \/ (A \ B1) = A by A16, A17, XBOOLE_1:45;

then dom ((max+ f) | (B1 \/ (A \ B1))) = (dom (max+ f)) /\ (dom (max+ f)) by A16, RELAT_1:61;

then (max+ f) | (B1 \/ (A \ B1)) = max+ f by A21, PARTFUN1:5;

then integral+ (M,(max+ f)) = (integral+ (M,((max+ f) | B1))) + (integral+ (M,((max+ f) | (A \ B1)))) by A1, A16, A19, Th81, XBOOLE_1:106;

then A22: integral+ (M,((max+ f) | B1)) <= integral+ (M,(max+ f)) by A1, A16, A19, Th80, XXREAL_3:65;

hereby :: thesis: ( M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

then reconsider B1 = B1 as measure_zero of M by MEASURE1:def 7;A23:
for r being Real st 0 < r holds

r * (M . B1) <= integral+ (M,(max+ f))

then A43: 0 < M . (f " {+infty}) by A12, Th45;

end;r * (M . B1) <= integral+ (M,(max+ f))

proof

assume A42:
M . (f " {+infty}) <> 0
; :: thesis: contradiction
defpred S_{1}[ object ] means $1 in dom ((max+ f) | B1);

let r be Real; :: thesis: ( 0 < r implies r * (M . B1) <= integral+ (M,(max+ f)) )

deffunc H_{1}( object ) -> Element of ExtREAL = In (r,ExtREAL);

A24: for x being object st S_{1}[x] holds

H_{1}(x) in ExtREAL
;

consider g being PartFunc of X,ExtREAL such that

A25: ( ( for x being object holds

( x in dom g iff ( x in X & S_{1}[x] ) ) ) & ( for x being object st x in dom g holds

g . x = H_{1}(x) ) )
from PARTFUN1:sch 3(A24);

assume A26: 0 < r ; :: thesis: r * (M . B1) <= integral+ (M,(max+ f))

then for x being object st x in dom g holds

0 <= g . x by A25;

then A27: g is nonnegative by SUPINF_2:52;

dom ((max+ f) | B1) = (dom (max+ f)) /\ B1 by RELAT_1:61;

then A28: dom ((max+ f) | B1) = B1 by A17, XBOOLE_1:28;

for x being object holds

( x in dom g iff ( x in X & x in dom ((max+ f) | B1) ) ) by A25;

then dom g = X /\ (dom ((max+ f) | B1)) by XBOOLE_0:def 4;

then A29: dom g = dom ((max+ f) | B1) by XBOOLE_1:28;

then A30: integral' (M,g) = r * (M . (dom g)) by A26, A25, A28, Th104;

A31: for x being Element of X st x in dom g holds

g . x <= ((max+ f) | B1) . x

then A35: B1 = (dom (chi (B1,X))) /\ B1 by XBOOLE_1:28;

then A36: (chi (B1,X)) | B1 is B1 -measurable by Th42, MESFUNC2:29;

A37: B1 = dom ((chi (B1,X)) | B1) by A35, RELAT_1:61;

A38: for x being Element of X st x in dom g holds

g . x = (r (#) ((chi (B1,X)) | B1)) . x

then g = r (#) ((chi (B1,X)) | B1) by A38, PARTFUN1:5;

then A41: g is B1 -measurable by A37, A36, MESFUNC1:37;

(max+ f) | B1 is nonnegative by Lm1, Th15;

then integral+ (M,g) <= integral+ (M,((max+ f) | B1)) by A20, A29, A28, A41, A27, A31, Th85;

then integral+ (M,g) <= integral+ (M,(max+ f)) by A22, XXREAL_0:2;

hence r * (M . B1) <= integral+ (M,(max+ f)) by A25, A29, A28, A27, A30, Lm4, Th77; :: thesis: verum

end;let r be Real; :: thesis: ( 0 < r implies r * (M . B1) <= integral+ (M,(max+ f)) )

deffunc H

A24: for x being object st S

H

consider g being PartFunc of X,ExtREAL such that

A25: ( ( for x being object holds

( x in dom g iff ( x in X & S

g . x = H

assume A26: 0 < r ; :: thesis: r * (M . B1) <= integral+ (M,(max+ f))

then for x being object st x in dom g holds

0 <= g . x by A25;

then A27: g is nonnegative by SUPINF_2:52;

dom ((max+ f) | B1) = (dom (max+ f)) /\ B1 by RELAT_1:61;

then A28: dom ((max+ f) | B1) = B1 by A17, XBOOLE_1:28;

for x being object holds

( x in dom g iff ( x in X & x in dom ((max+ f) | B1) ) ) by A25;

then dom g = X /\ (dom ((max+ f) | B1)) by XBOOLE_0:def 4;

then A29: dom g = dom ((max+ f) | B1) by XBOOLE_1:28;

then A30: integral' (M,g) = r * (M . (dom g)) by A26, A25, A28, Th104;

A31: for x being Element of X st x in dom g holds

g . x <= ((max+ f) | B1) . x

proof

dom (chi (B1,X)) = X
by FUNCT_3:def 3;
let x be Element of X; :: thesis: ( x in dom g implies g . x <= ((max+ f) | B1) . x )

assume A32: x in dom g ; :: thesis: g . x <= ((max+ f) | B1) . x

then x in dom f by A29, A28, FUNCT_1:def 7;

then A33: x in dom (max+ f) by MESFUNC2:def 2;

f . x in {+infty} by A29, A28, A32, FUNCT_1:def 7;

then A34: f . x = +infty by TARSKI:def 1;

then max ((f . x),0) = f . x by XXREAL_0:def 10;

then (max+ f) . x = +infty by A34, A33, MESFUNC2:def 2;

then ((max+ f) | B1) . x = +infty by A29, A28, A32, FUNCT_1:49;

hence g . x <= ((max+ f) | B1) . x by XXREAL_0:4; :: thesis: verum

end;assume A32: x in dom g ; :: thesis: g . x <= ((max+ f) | B1) . x

then x in dom f by A29, A28, FUNCT_1:def 7;

then A33: x in dom (max+ f) by MESFUNC2:def 2;

f . x in {+infty} by A29, A28, A32, FUNCT_1:def 7;

then A34: f . x = +infty by TARSKI:def 1;

then max ((f . x),0) = f . x by XXREAL_0:def 10;

then (max+ f) . x = +infty by A34, A33, MESFUNC2:def 2;

then ((max+ f) | B1) . x = +infty by A29, A28, A32, FUNCT_1:49;

hence g . x <= ((max+ f) | B1) . x by XXREAL_0:4; :: thesis: verum

then A35: B1 = (dom (chi (B1,X))) /\ B1 by XBOOLE_1:28;

then A36: (chi (B1,X)) | B1 is B1 -measurable by Th42, MESFUNC2:29;

A37: B1 = dom ((chi (B1,X)) | B1) by A35, RELAT_1:61;

A38: for x being Element of X st x in dom g holds

g . x = (r (#) ((chi (B1,X)) | B1)) . x

proof

dom g = dom (r (#) ((chi (B1,X)) | B1))
by A29, A28, A37, MESFUNC1:def 6;
let x be Element of X; :: thesis: ( x in dom g implies g . x = (r (#) ((chi (B1,X)) | B1)) . x )

assume A39: x in dom g ; :: thesis: g . x = (r (#) ((chi (B1,X)) | B1)) . x

then x in dom ((chi (B1,X)) | B1) by A29, A28, A35, RELAT_1:61;

then x in dom (r (#) ((chi (B1,X)) | B1)) by MESFUNC1:def 6;

then A40: (r (#) ((chi (B1,X)) | B1)) . x = r * (((chi (B1,X)) | B1) . x) by MESFUNC1:def 6

.= r * ((chi (B1,X)) . x) by A29, A28, A37, A39, FUNCT_1:47 ;

(chi (B1,X)) . x = 1 by A29, A28, A39, FUNCT_3:def 3;

then (r (#) ((chi (B1,X)) | B1)) . x = r by A40, XXREAL_3:81;

hence g . x = (r (#) ((chi (B1,X)) | B1)) . x by A25, A39; :: thesis: verum

end;assume A39: x in dom g ; :: thesis: g . x = (r (#) ((chi (B1,X)) | B1)) . x

then x in dom ((chi (B1,X)) | B1) by A29, A28, A35, RELAT_1:61;

then x in dom (r (#) ((chi (B1,X)) | B1)) by MESFUNC1:def 6;

then A40: (r (#) ((chi (B1,X)) | B1)) . x = r * (((chi (B1,X)) | B1) . x) by MESFUNC1:def 6

.= r * ((chi (B1,X)) . x) by A29, A28, A37, A39, FUNCT_1:47 ;

(chi (B1,X)) . x = 1 by A29, A28, A39, FUNCT_3:def 3;

then (r (#) ((chi (B1,X)) | B1)) . x = r by A40, XXREAL_3:81;

hence g . x = (r (#) ((chi (B1,X)) | B1)) . x by A25, A39; :: thesis: verum

then g = r (#) ((chi (B1,X)) | B1) by A38, PARTFUN1:5;

then A41: g is B1 -measurable by A37, A36, MESFUNC1:37;

(max+ f) | B1 is nonnegative by Lm1, Th15;

then integral+ (M,g) <= integral+ (M,((max+ f) | B1)) by A20, A29, A28, A41, A27, A31, Th85;

then integral+ (M,g) <= integral+ (M,(max+ f)) by A22, XXREAL_0:2;

hence r * (M . B1) <= integral+ (M,(max+ f)) by A25, A29, A28, A27, A30, Lm4, Th77; :: thesis: verum

then A43: 0 < M . (f " {+infty}) by A12, Th45;

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

end;

suppose A44:
M . B1 = +infty
; :: thesis: contradiction

jj * (M . B1) <= integral+ (M,(max+ f))
by A23;

hence contradiction by A3, A44, XXREAL_3:81; :: thesis: verum

end;hence contradiction by A3, A44, XXREAL_3:81; :: thesis: verum

suppose
M . B1 <> +infty
; :: thesis: contradiction

then reconsider MB = M . B1 as Element of REAL by A43, XXREAL_0:14;

jj * (M . B1) <= integral+ (M,(max+ f)) by A23;

then A45: 0 < integral+ (M,(max+ f)) by A43;

then reconsider I = integral+ (M,(max+ f)) as Element of REAL by A3, XXREAL_0:14;

A46: ((2 * I) / MB) * (M . B1) = ((2 * I) / MB) * MB ;

((2 * I) / MB) * (M . B1) <= integral+ (M,(max+ f)) by A43, A23, A45;

then 2 * I <= I by A42, A46, XCMPLX_1:87;

hence contradiction by A45, XREAL_1:155; :: thesis: verum

end;jj * (M . B1) <= integral+ (M,(max+ f)) by A23;

then A45: 0 < integral+ (M,(max+ f)) by A43;

then reconsider I = integral+ (M,(max+ f)) as Element of REAL by A3, XXREAL_0:14;

A46: ((2 * I) / MB) * (M . B1) = ((2 * I) / MB) * MB ;

((2 * I) / MB) * (M . B1) <= integral+ (M,(max+ f)) by A43, A23, A45;

then 2 * I <= I by A42, A46, XCMPLX_1:87;

hence contradiction by A45, XREAL_1:155; :: thesis: verum

A47: max- f is nonnegative by Lm1;

A48: A = dom (max- f) by A4, MESFUNC2:def 3;

then A49: B2 c= dom (max- f) by A9, Th30;

then A50: B2 = (dom (max- f)) /\ B2 by XBOOLE_1:28;

A51: max- f is A -measurable by A4, A5, MESFUNC2:26;

then max- f is B2 -measurable by A48, A49, MESFUNC1:30;

then A52: (max- f) | B2 is B2 -measurable by A50, Th42;

B2 \/ (A \ B2) = A by A48, A49, XBOOLE_1:45;

then dom ((max- f) | (B2 \/ (A \ B2))) = (dom (max- f)) /\ (dom (max- f)) by A48, RELAT_1:61;

then (max- f) | (B2 \/ (A \ B2)) = max- f by A21, PARTFUN1:5;

then integral+ (M,(max- f)) = (integral+ (M,((max- f) | B2))) + (integral+ (M,((max- f) | (A \ B2)))) by A47, A48, A51, Th81, XBOOLE_1:106;

then A53: integral+ (M,((max- f) | B2)) <= integral+ (M,(max- f)) by A47, A48, A51, Th80, XXREAL_3:65;

hereby :: thesis: ( (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

thus
(f " {+infty}) \/ (f " {-infty}) in S
by A12, A14, PROB_1:3; :: thesis: M . ((f " {+infty}) \/ (f " {-infty})) = 0 A55:
for r being Real st 0 < r holds

r * (M . B2) <= integral+ (M,(max- f))

A75: 0 <= M . (f " {-infty}) by A14, Th45;

end;r * (M . B2) <= integral+ (M,(max- f))

proof

assume A74:
M . (f " {-infty}) <> 0
; :: thesis: contradiction
defpred S_{1}[ object ] means $1 in dom ((max- f) | B2);

let r be Real; :: thesis: ( 0 < r implies r * (M . B2) <= integral+ (M,(max- f)) )

deffunc H_{1}( object ) -> Element of ExtREAL = In (r,ExtREAL);

A56: for x being object st S_{1}[x] holds

H_{1}(x) in ExtREAL
;

consider g being PartFunc of X,ExtREAL such that

A57: ( ( for x being object holds

( x in dom g iff ( x in X & S_{1}[x] ) ) ) & ( for x being object st x in dom g holds

g . x = H_{1}(x) ) )
from PARTFUN1:sch 3(A56);

assume A58: 0 < r ; :: thesis: r * (M . B2) <= integral+ (M,(max- f))

then for x being object st x in dom g holds

0 <= g . x by A57;

then A59: g is nonnegative by SUPINF_2:52;

dom ((max- f) | B2) = (dom (max- f)) /\ B2 by RELAT_1:61;

then A60: dom ((max- f) | B2) = B2 by A49, XBOOLE_1:28;

for x being object holds

( x in dom g iff ( x in X & x in dom ((max- f) | B2) ) ) by A57;

then dom g = X /\ (dom ((max- f) | B2)) by XBOOLE_0:def 4;

then A61: dom g = dom ((max- f) | B2) by XBOOLE_1:28;

then A62: integral' (M,g) = r * (M . (dom g)) by A58, A57, A60, Th104;

dom (chi (B2,X)) = X by FUNCT_3:def 3;

then A63: B2 = (dom (chi (B2,X))) /\ B2 by XBOOLE_1:28;

then A64: B2 = dom ((chi (B2,X)) | B2) by RELAT_1:61;

A65: for x being Element of X st x in dom g holds

g . x = (r (#) ((chi (B2,X)) | B2)) . x

g . x <= ((max- f) | B2) . x

dom g = dom (r (#) ((chi (B2,X)) | B2)) by A61, A60, A64, MESFUNC1:def 6;

then g = r (#) ((chi (B2,X)) | B2) by A65, PARTFUN1:5;

then A73: g is B2 -measurable by A64, A72, MESFUNC1:37;

(max- f) | B2 is nonnegative by Lm1, Th15;

then integral+ (M,g) <= integral+ (M,((max- f) | B2)) by A52, A61, A60, A73, A59, A68, Th85;

then integral+ (M,g) <= integral+ (M,(max- f)) by A53, XXREAL_0:2;

hence r * (M . B2) <= integral+ (M,(max- f)) by A57, A61, A60, A59, A62, Lm4, Th77; :: thesis: verum

end;let r be Real; :: thesis: ( 0 < r implies r * (M . B2) <= integral+ (M,(max- f)) )

deffunc H

A56: for x being object st S

H

consider g being PartFunc of X,ExtREAL such that

A57: ( ( for x being object holds

( x in dom g iff ( x in X & S

g . x = H

assume A58: 0 < r ; :: thesis: r * (M . B2) <= integral+ (M,(max- f))

then for x being object st x in dom g holds

0 <= g . x by A57;

then A59: g is nonnegative by SUPINF_2:52;

dom ((max- f) | B2) = (dom (max- f)) /\ B2 by RELAT_1:61;

then A60: dom ((max- f) | B2) = B2 by A49, XBOOLE_1:28;

for x being object holds

( x in dom g iff ( x in X & x in dom ((max- f) | B2) ) ) by A57;

then dom g = X /\ (dom ((max- f) | B2)) by XBOOLE_0:def 4;

then A61: dom g = dom ((max- f) | B2) by XBOOLE_1:28;

then A62: integral' (M,g) = r * (M . (dom g)) by A58, A57, A60, Th104;

dom (chi (B2,X)) = X by FUNCT_3:def 3;

then A63: B2 = (dom (chi (B2,X))) /\ B2 by XBOOLE_1:28;

then A64: B2 = dom ((chi (B2,X)) | B2) by RELAT_1:61;

A65: for x being Element of X st x in dom g holds

g . x = (r (#) ((chi (B2,X)) | B2)) . x

proof

A68:
for x being Element of X st x in dom g holds
let x be Element of X; :: thesis: ( x in dom g implies g . x = (r (#) ((chi (B2,X)) | B2)) . x )

assume A66: x in dom g ; :: thesis: g . x = (r (#) ((chi (B2,X)) | B2)) . x

then x in dom (r (#) ((chi (B2,X)) | B2)) by A61, A60, A64, MESFUNC1:def 6;

then A67: (r (#) ((chi (B2,X)) | B2)) . x = r * (((chi (B2,X)) | B2) . x) by MESFUNC1:def 6

.= r * ((chi (B2,X)) . x) by A61, A60, A64, A66, FUNCT_1:47 ;

(chi (B2,X)) . x = 1 by A61, A60, A66, FUNCT_3:def 3;

then (r (#) ((chi (B2,X)) | B2)) . x = r by A67, XXREAL_3:81;

hence g . x = (r (#) ((chi (B2,X)) | B2)) . x by A57, A66; :: thesis: verum

end;assume A66: x in dom g ; :: thesis: g . x = (r (#) ((chi (B2,X)) | B2)) . x

then x in dom (r (#) ((chi (B2,X)) | B2)) by A61, A60, A64, MESFUNC1:def 6;

then A67: (r (#) ((chi (B2,X)) | B2)) . x = r * (((chi (B2,X)) | B2) . x) by MESFUNC1:def 6

.= r * ((chi (B2,X)) . x) by A61, A60, A64, A66, FUNCT_1:47 ;

(chi (B2,X)) . x = 1 by A61, A60, A66, FUNCT_3:def 3;

then (r (#) ((chi (B2,X)) | B2)) . x = r by A67, XXREAL_3:81;

hence g . x = (r (#) ((chi (B2,X)) | B2)) . x by A57, A66; :: thesis: verum

g . x <= ((max- f) | B2) . x

proof

A72:
(chi (B2,X)) | B2 is B2 -measurable
by A63, Th42, MESFUNC2:29;
let x be Element of X; :: thesis: ( x in dom g implies g . x <= ((max- f) | B2) . x )

assume A69: x in dom g ; :: thesis: g . x <= ((max- f) | B2) . x

then x in dom f by A61, A60, FUNCT_1:def 7;

then A70: x in dom (max- f) by MESFUNC2:def 3;

f . x in {-infty} by A61, A60, A69, FUNCT_1:def 7;

then A71: - (f . x) = +infty by TARSKI:def 1, XXREAL_3:5;

then max ((- (f . x)),0) = - (f . x) by XXREAL_0:def 10;

then (max- f) . x = +infty by A71, A70, MESFUNC2:def 3;

then ((max- f) | B2) . x = +infty by A61, A60, A69, FUNCT_1:49;

hence g . x <= ((max- f) | B2) . x by XXREAL_0:4; :: thesis: verum

end;assume A69: x in dom g ; :: thesis: g . x <= ((max- f) | B2) . x

then x in dom f by A61, A60, FUNCT_1:def 7;

then A70: x in dom (max- f) by MESFUNC2:def 3;

f . x in {-infty} by A61, A60, A69, FUNCT_1:def 7;

then A71: - (f . x) = +infty by TARSKI:def 1, XXREAL_3:5;

then max ((- (f . x)),0) = - (f . x) by XXREAL_0:def 10;

then (max- f) . x = +infty by A71, A70, MESFUNC2:def 3;

then ((max- f) | B2) . x = +infty by A61, A60, A69, FUNCT_1:49;

hence g . x <= ((max- f) | B2) . x by XXREAL_0:4; :: thesis: verum

dom g = dom (r (#) ((chi (B2,X)) | B2)) by A61, A60, A64, MESFUNC1:def 6;

then g = r (#) ((chi (B2,X)) | B2) by A65, PARTFUN1:5;

then A73: g is B2 -measurable by A64, A72, MESFUNC1:37;

(max- f) | B2 is nonnegative by Lm1, Th15;

then integral+ (M,g) <= integral+ (M,((max- f) | B2)) by A52, A61, A60, A73, A59, A68, Th85;

then integral+ (M,g) <= integral+ (M,(max- f)) by A53, XXREAL_0:2;

hence r * (M . B2) <= integral+ (M,(max- f)) by A57, A61, A60, A59, A62, Lm4, Th77; :: thesis: verum

A75: 0 <= M . (f " {-infty}) by A14, Th45;

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

end;

suppose A76:
M . B2 = +infty
; :: thesis: contradiction

jj * (M . B2) <= integral+ (M,(max- f))
by A55;

hence contradiction by A15, A76, XXREAL_3:81; :: thesis: verum

end;hence contradiction by A15, A76, XXREAL_3:81; :: thesis: verum

suppose
M . B2 <> +infty
; :: thesis: contradiction

then reconsider MB = M . B2 as Element of REAL by A75, XXREAL_0:14;

jj * (M . B2) <= integral+ (M,(max- f)) by A55;

then A77: 0 < integral+ (M,(max- f)) by A74, A75;

then reconsider I = integral+ (M,(max- f)) as Element of REAL by A15, XXREAL_0:14;

A78: ((2 * I) / MB) * (M . B2) = ((2 * I) / MB) * MB ;

((2 * I) / MB) * (M . B2) <= integral+ (M,(max- f)) by A74, A75, A55, A77;

then 2 * I <= I by A74, A78, XCMPLX_1:87;

hence contradiction by A77, XREAL_1:155; :: thesis: verum

end;jj * (M . B2) <= integral+ (M,(max- f)) by A55;

then A77: 0 < integral+ (M,(max- f)) by A74, A75;

then reconsider I = integral+ (M,(max- f)) as Element of REAL by A15, XXREAL_0:14;

A78: ((2 * I) / MB) * (M . B2) = ((2 * I) / MB) * MB ;

((2 * I) / MB) * (M . B2) <= integral+ (M,(max- f)) by A74, A75, A55, A77;

then 2 * I <= I by A74, A78, XCMPLX_1:87;

hence contradiction by A77, XREAL_1:155; :: thesis: verum

thus M . ((f " {+infty}) \/ (f " {-infty})) = M . (B1 \/ B2)

.= 0 by A54, MEASURE1:38 ; :: thesis: verum