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;

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

A23: for r being Real st 0 < r holds
r * (M . B1) <= integral+ (M,(max+ f))

proof

defpred S₁[ 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₁( object ) -> Element of ExtREAL = In (r,ExtREAL);
A24: for x being object st S₁[x] holds
H₁(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₁[x] ) ) ) & ( for x being object st x in dom g holds
g . x = H₁(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

proof

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;

dom (chi (B1,X)) = X by FUNCT_3:def 3;
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

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;

dom g = dom (r (#) ((chi (B1,X)) | B1)) by A29, A28, A37, MESFUNC1:def 6;
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;

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

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

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;

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;

end;

end;

then reconsider B1 = B1 as measure_zero of M by MEASURE1:def 7;
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 )

A55: for r being Real st 0 < r holds
r * (M . B2) <= integral+ (M,(max- f))

proof

defpred S₁[ 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₁( object ) -> Element of ExtREAL = In (r,ExtREAL);
A56: for x being object st S₁[x] holds
H₁(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₁[x] ) ) ) & ( for x being object st x in dom g holds
g . x = H₁(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

proof

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;

A68: for x being Element of X st x in dom g holds
g . x <= ((max- f) | B2) . x

proof

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;

A72: (chi (B2,X)) | B2 is B2 -measurable by A63, Th42, MESFUNC2:29;
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;

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

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

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;

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;

end;

end;

thus (f " {+infty}) \/ (f " {-infty}) in S by A12, A14, PROB_1:3; :: thesis: M . ((f " {+infty}) \/ (f " {-infty})) = 0
thus M . ((f " {+infty}) \/ (f " {-infty})) = M . (B1 \/ B2)
.= 0 by A54, MEASURE1:38 ; :: thesis: verum