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 by Def17;
consider A being Element of S such that
A4: A = dom f and
A5: f is_measurable_on A by A2, Def17;
A6: for x being set 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 16;
then A7: eq_dom (f,+infty) c= A by TARSKI:def 3;
then A8: A /\ (eq_dom (f,+infty)) = eq_dom (f,+infty) by XBOOLE_1:28;
A9: eq_dom (f,-infty) c= A by A6, TARSKI:def 3;
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:37;
then A12: f " {+infty} in S by A8, Th36;
A13: A /\ (eq_dom (f,-infty)) in S by A5, MESFUNC1:38;
then reconsider B2 = f " {-infty} as Element of S by A10, Th36;
A14: f " {-infty} in S by A13, A10, Th36;
thus ( f " {+infty} in S & f " {-infty} in S ) by A11, A13, A8, A10, Th36; :: 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, Def17;
reconsider B1 = f " {+infty} as Element of S by A11, A8, Th36;
A16: A = dom (max+ f) by A4, MESFUNC2:def 2;
then A17: B1 c= dom (max+ f) by A7, Th36;
then A18: B1 = (dom (max+ f)) /\ B1 by XBOOLE_1:28;
A19: max+ f is_measurable_on A by A5, MESFUNC2:27;
then max+ f is_measurable_on B1 by A16, A17, MESFUNC1:34;
then A20: (max+ f) | B1 is_measurable_on B1 by A18, Th48;
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:70;
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:90;
then (max+ f) | (B1 \/ (A \ B1)) = max+ f by A21, PARTFUN1:34;
then integral+ (M,(max+ f)) = (integral+ (M,((max+ f) | B1))) + (integral+ (M,((max+ f) | (A \ B1)))) by A1, A16, A19, Th87, XBOOLE_1:106;
then A22: integral+ (M,((max+ f) | B1)) <= integral+ (M,(max+ f)) by A1, A16, A19, Th86, XXREAL_3:76;

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_EAL r) * (M . B1) <= integral+ (M,(max+ f))

proof

defpred S₁[ set ] means $1 in dom ((max+ f) | B1);
let r be Real; :: thesis: ( 0 < r implies (R_EAL r) * (M . B1) <= integral+ (M,(max+ f)) )
deffunc H₁( set ) -> Element of ExtREAL = R_EAL r;
A24: for x being set st S₁[x] holds
H₁(x) in ExtREAL ;
consider g being PartFunc of X,ExtREAL such that
A25: ( ( for x being set holds
( x in dom g iff ( x in X & S₁[x] ) ) ) & ( for x being set st x in dom g holds
g . x = H₁(x) ) ) from PARTFUN1:sch 3(A24);
assume A26: 0 < r ; :: thesis: (R_EAL r) * (M . B1) <= integral+ (M,(max+ f))
then for x being set st x in dom g holds
0 <= g . x by A25;
then A27: g is nonnegative by SUPINF_2:71;
dom ((max+ f) | B1) = (dom (max+ f)) /\ B1 by RELAT_1:90;
then A28: dom ((max+ f) | B1) = B1 by A17, XBOOLE_1:28;
dom g = X /\ (dom ((max+ f) | B1)) by A25, XBOOLE_0:def 4;
then A29: dom g = dom ((max+ f) | B1) by XBOOLE_1:28;
then A30: integral' (M,g) = (R_EAL r) * (M . (dom g)) by A26, A25, A28, Th110;
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 13;
then A33: x in dom (max+ f) by MESFUNC2:def 2;
f . x in {+infty} by A29, A28, A32, FUNCT_1:def 13;
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:72;
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_measurable_on B1 by Th48, MESFUNC2:32;
A37: B1 = dom ((chi (B1,X)) | B1) by A35, RELAT_1:90;
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:90;
then x in dom (r (#) ((chi (B1,X)) | B1)) by MESFUNC1:def 6;
then A40: (r (#) ((chi (B1,X)) | B1)) . x = (R_EAL r) * (((chi (B1,X)) | B1) . x) by MESFUNC1:def 6
.= (R_EAL r) * ((chi (B1,X)) . x) by A29, A28, A37, A39, FUNCT_1:70 ;
(chi (B1,X)) . x = 1 by A29, A28, A39, FUNCT_3:def 3;
then (r (#) ((chi (B1,X)) | B1)) . x = R_EAL r by A40, XXREAL_3:92;
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:34;
then A41: g is_measurable_on B1 by A37, A36, MESFUNC1:41;
(max+ f) | B1 is nonnegative by Lm1, Th21;
then integral+ (M,g) <= integral+ (M,((max+ f) | B1)) by A20, A29, A28, A41, A27, A31, Th91;
then integral+ (M,g) <= integral+ (M,(max+ f)) by A22, XXREAL_0:2;
hence (R_EAL r) * (M . B1) <= integral+ (M,(max+ f)) by A25, A29, A28, A27, A30, Lm4, Th83; :: thesis: verum

end;

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

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

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

(R_EAL 1) * (M . B1) <= integral+ (M,(max+ f)) by A23;
hence contradiction by A3, A44, XXREAL_3:92; :: thesis: verum

end;

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

then reconsider MB = M . B1 as Real by A43, XXREAL_0:14;
(R_EAL 1) * (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 Real by A3, XXREAL_0:14;
A46: (R_EAL ((2 * I) / MB)) * (M . B1) = ((2 * I) / MB) * MB by EXTREAL1:13;
(R_EAL ((2 * I) / MB)) * (M . B1) <= integral+ (M,(max+ f)) by A43, A23, A45;
then 2 * I <= I by A42, A46, XCMPLX_1:88;
hence contradiction by A45, XREAL_1:157; :: thesis: verum

end;

end;

end;

then reconsider B1 = B1 as measure_zero of M by MEASURE1:def 13;
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, Th36;
then A50: B2 = (dom (max- f)) /\ B2 by XBOOLE_1:28;
A51: max- f is_measurable_on A by A4, A5, MESFUNC2:28;
then max- f is_measurable_on B2 by A48, A49, MESFUNC1:34;
then A52: (max- f) | B2 is_measurable_on B2 by A50, Th48;
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:90;
then (max- f) | (B2 \/ (A \ B2)) = max- f by A21, PARTFUN1:34;
then integral+ (M,(max- f)) = (integral+ (M,((max- f) | B2))) + (integral+ (M,((max- f) | (A \ B2)))) by A47, A48, A51, Th87, XBOOLE_1:106;
then A53: integral+ (M,((max- f) | B2)) <= integral+ (M,(max- f)) by A47, A48, A51, Th86, XXREAL_3:76;

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

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

proof

defpred S₁[ set ] means $1 in dom ((max- f) | B2);
let r be Real; :: thesis: ( 0 < r implies (R_EAL r) * (M . B2) <= integral+ (M,(max- f)) )
deffunc H₁( set ) -> Element of ExtREAL = R_EAL r;
A56: for x being set st S₁[x] holds
H₁(x) in ExtREAL ;
consider g being PartFunc of X,ExtREAL such that
A57: ( ( for x being set holds
( x in dom g iff ( x in X & S₁[x] ) ) ) & ( for x being set st x in dom g holds
g . x = H₁(x) ) ) from PARTFUN1:sch 3(A56);
assume A58: 0 < r ; :: thesis: (R_EAL r) * (M . B2) <= integral+ (M,(max- f))
then for x being set st x in dom g holds
0 <= g . x by A57;
then A59: g is nonnegative by SUPINF_2:71;
dom ((max- f) | B2) = (dom (max- f)) /\ B2 by RELAT_1:90;
then A60: dom ((max- f) | B2) = B2 by A49, XBOOLE_1:28;
dom g = X /\ (dom ((max- f) | B2)) by A57, XBOOLE_0:def 4;
then A61: dom g = dom ((max- f) | B2) by XBOOLE_1:28;
then A62: integral' (M,g) = (R_EAL r) * (M . (dom g)) by A58, A57, A60, Th110;
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:90;
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_EAL r) * (((chi (B2,X)) | B2) . x) by MESFUNC1:def 6
.= (R_EAL r) * ((chi (B2,X)) . x) by A61, A60, A64, A66, FUNCT_1:70 ;
(chi (B2,X)) . x = 1 by A61, A60, A66, FUNCT_3:def 3;
then (r (#) ((chi (B2,X)) | B2)) . x = R_EAL r by A67, XXREAL_3:92;
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 13;
then A70: x in dom (max- f) by MESFUNC2:def 3;
f . x in {-infty} by A61, A60, A69, FUNCT_1:def 13;
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:72;
hence g . x <= ((max- f) | B2) . x by XXREAL_0:4; :: thesis: verum

end;

A72: (chi (B2,X)) | B2 is_measurable_on B2 by A63, Th48, MESFUNC2:32;
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:34;
then A73: g is_measurable_on B2 by A64, A72, MESFUNC1:41;
(max- f) | B2 is nonnegative by Lm1, Th21;
then integral+ (M,g) <= integral+ (M,((max- f) | B2)) by A52, A61, A60, A73, A59, A68, Th91;
then integral+ (M,g) <= integral+ (M,(max- f)) by A53, XXREAL_0:2;
hence (R_EAL r) * (M . B2) <= integral+ (M,(max- f)) by A57, A61, A60, A59, A62, Lm4, Th83; :: thesis: verum

end;

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

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

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

(R_EAL 1) * (M . B2) <= integral+ (M,(max- f)) by A55;
hence contradiction by A15, A76, XXREAL_3:92; :: thesis: verum

end;

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

then reconsider MB = M . B2 as Real by A75, XXREAL_0:14;
(R_EAL 1) * (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 Real by A15, XXREAL_0:14;
A78: (R_EAL ((2 * I) / MB)) * (M . B2) = ((2 * I) / MB) * MB by EXTREAL1:13;
(R_EAL ((2 * I) / MB)) * (M . B2) <= integral+ (M,(max- f)) by A74, A75, A55, A77;
then 2 * I <= I by A74, A78, XCMPLX_1:88;
hence contradiction by A77, XREAL_1:157; :: thesis: verum

end;

end;

end;

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