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 ) )
assume A1: 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 A2: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & integral+ M,(max+ f) < +infty & integral+ M,(max- f) < +infty ) by Def17;
consider A being Element of S such that
A3: ( A = dom f & f is_measurable_on A ) by A1, Def17;
A4: ( A /\ (eq_dom f,+infty ) in S & A /\ (eq_dom f,-infty ) in S ) by A3, MESFUNC1:37, MESFUNC1:38;
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 A3, MESFUNC1:def 16;
then A5: ( eq_dom f,+infty c= A & eq_dom f,-infty c= A ) by TARSKI:def 3;
then A6: ( A /\ (eq_dom f,+infty ) = eq_dom f,+infty & A /\ (eq_dom f,-infty ) = eq_dom f,-infty ) by XBOOLE_1:28;
then A7: ( f " {+infty } in S & f " {-infty } in S ) by A4, Th36;
thus ( f " {+infty } in S & f " {-infty } in S ) by A4, A6, Th36; :: thesis: ( M . (f " {+infty }) = 0 & M . (f " {-infty }) = 0 & (f " {+infty }) \/ (f " {-infty }) in S & M . ((f " {+infty }) \/ (f " {-infty })) = 0 )
reconsider B1 = f " {+infty } as Element of S by A4, A6, Th36;
reconsider B2 = f " {-infty } as Element of S by A4, A6, Th36;
A8: ( max+ f is nonnegative & max- f is nonnegative ) by Lm1;
set C1 = A \ B1;
set C2 = A \ B2;
A9: ( A = dom (max+ f) & A = dom (max- f) ) by A3, MESFUNC2:def 2, MESFUNC2:def 3;
then A10: ( B1 c= dom (max+ f) & B2 c= dom (max- f) ) by A5, Th36;
then ( B1 \/ (A \ B1) = A & B2 \/ (A \ B2) = A ) by A9, XBOOLE_1:45;
then A11: ( dom ((max+ f) | (B1 \/ (A \ B1))) = (dom (max+ f)) /\ (dom (max+ f)) & dom ((max- f) | (B2 \/ (A \ B2))) = (dom (max- f)) /\ (dom (max- f)) ) by A9, RELAT_1:90;
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;
then A12: ( (max+ f) | (B1 \/ (A \ B1)) = max+ f & (max- f) | (B2 \/ (A \ B2)) = max- f ) by A11, PARTFUN1:34;
A13: ( max+ f is_measurable_on A & max- f is_measurable_on A ) by A3, MESFUNC2:27, MESFUNC2:28;
then A14: ( max+ f is_measurable_on B1 & max- f is_measurable_on B2 ) by A9, A10, MESFUNC1:34;
( B1 = (dom (max+ f)) /\ B1 & B2 = (dom (max- f)) /\ B2 ) by A10, XBOOLE_1:28;
then A15: ( (max+ f) | B1 is_measurable_on B1 & (max- f) | B2 is_measurable_on B2 ) by A14, Th48;
( 0 <= integral+ M,((max+ f) | (A \ B1)) & 0 <= integral+ M,((max+ f) | B1) & integral+ M,(max+ f) = (integral+ M,((max+ f) | B1)) + (integral+ M,((max+ f) | (A \ B1))) & 0 <= integral+ M,((max- f) | (A \ B2)) & 0 <= integral+ M,((max- f) | B2) & integral+ M,(max- f) = (integral+ M,((max- f) | B2)) + (integral+ M,((max- f) | (A \ B2))) ) by A8, A9, A12, A13, Th86, Th87, XBOOLE_1:106;
then A16: ( integral+ M,((max+ f) | B1) <= integral+ M,(max+ f) & integral+ M,((max- f) | B2) <= integral+ M,(max- f) ) by XXREAL_3:76;

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

assume A18: M . (f " {+infty }) <> 0 ; :: thesis: contradiction
then A19: 0 < M . (f " {+infty }) by A7, Th51;
A20: for r being Real st 0 < r holds
(R_EAL r) * (M . B1) <= integral+ M,(max+ f)

proof

let r be Real; :: thesis: ( 0 < r implies (R_EAL r) * (M . B1) <= integral+ M,(max+ f) )
assume A21: 0 < r ; :: thesis: (R_EAL r) * (M . B1) <= integral+ M,(max+ f)
defpred S₁[ set ] means $1 in dom ((max+ f) | B1);
deffunc H₁( set ) -> Element of ExtREAL = R_EAL r;
A22: for x being set st S₁[x] holds
H₁(x) in ExtREAL ;
consider g being PartFunc of X,ExtREAL such that
A23: ( ( 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(A22);
dom g = X /\ (dom ((max+ f) | B1)) by A23, XBOOLE_0:def 4;
then A24: dom g = dom ((max+ f) | B1) by XBOOLE_1:28;
dom ((max+ f) | B1) = (dom (max+ f)) /\ B1 by RELAT_1:90;
then A25: dom ((max+ f) | B1) = B1 by A10, XBOOLE_1:28;
A26: g is_measurable_on B1

proof

dom (chi B1,X) = X by FUNCT_3:def 3;
then A27: B1 = (dom (chi B1,X)) /\ B1 by XBOOLE_1:28;
then A28: B1 = dom ((chi B1,X) | B1) by RELAT_1:90;
then A29: dom g = dom (r (#) ((chi B1,X) | B1)) by A24, A25, MESFUNC1:def 6;
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 A30: x in dom g ; :: thesis: g . x = (r (#) ((chi B1,X) | B1)) . x
then x in dom ((chi B1,X) | B1) by A24, A25, A27, RELAT_1:90;
then x in dom (r (#) ((chi B1,X) | B1)) by MESFUNC1:def 6;
then A31: (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 A24, A25, A28, A30, FUNCT_1:70 ;
(chi B1,X) . x = 1 by A24, A25, A30, FUNCT_3:def 3;
then (r (#) ((chi B1,X) | B1)) . x = R_EAL r by A31, XXREAL_3:92;
hence g . x = (r (#) ((chi B1,X) | B1)) . x by A23, A30; :: thesis: verum

end;

then A32: g = r (#) ((chi B1,X) | B1) by A29, PARTFUN1:34;
(chi B1,X) | B1 is_measurable_on B1 by A27, Th48, MESFUNC2:32;
hence g is_measurable_on B1 by A28, A32, MESFUNC1:41; :: thesis: verum

end;

for x being set st x in dom g holds
0 <= g . x by A21, A23;
then A33: g is nonnegative by SUPINF_2:71;
A34: 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 A35: x in dom g ; :: thesis: g . x <= ((max+ f) | B1) . x
then A36: ( x in dom f & f . x in {+infty } ) by A24, A25, FUNCT_1:def 13;
then A37: f . x = +infty by TARSKI:def 1;
then A38: max (f . x),0 = f . x by XXREAL_0:def 10;
x in dom (max+ f) by A36, MESFUNC2:def 2;
then (max+ f) . x = +infty by A37, A38, MESFUNC2:def 2;
then ((max+ f) | B1) . x = +infty by A24, A25, A35, FUNCT_1:72;
hence g . x <= ((max+ f) | B1) . x by XXREAL_0:4; :: thesis: verum

end;

(max+ f) | B1 is nonnegative by Lm1, Th21;
then integral+ M,g <= integral+ M,((max+ f) | B1) by A15, A24, A25, A26, A33, A34, Th91;
then A39: integral+ M,g <= integral+ M,(max+ f) by A16, XXREAL_0:2;
integral' M,g = (R_EAL r) * (M . (dom g)) by A21, A23, A24, A25, Th110;
hence (R_EAL r) * (M . B1) <= integral+ M,(max+ f) by A33, A39, A23, A24, A25, Lm5, Th83; :: thesis: verum

end;

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

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

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

end;

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

(R_EAL 1) * (M . B1) <= integral+ M,(max+ f) by A20;
then A43: 0 < integral+ M,(max+ f) by A19;
reconsider MB = M . B1 as Real by A19, A42, XXREAL_0:14;
reconsider I = integral+ M,(max+ f) as Real by A2, A43, XXREAL_0:14;
A44: (R_EAL ((2 * I) / MB)) * (M . B1) <= integral+ M,(max+ f) by A19, A20, A43;
(R_EAL ((2 * I) / MB)) * (M . B1) = ((2 * I) / MB) * MB by EXTREAL1:13;
then 2 * I <= I by A18, A44, XCMPLX_1:88;
hence contradiction by A43, XREAL_1:157; :: thesis: verum

end;

end;

end;

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

assume A46: M . (f " {-infty }) <> 0 ; :: thesis: contradiction
A47: 0 <= M . (f " {-infty }) by A7, Th51;
A48: for r being Real st 0 < r holds
(R_EAL r) * (M . B2) <= integral+ M,(max- f)

proof

let r be Real; :: thesis: ( 0 < r implies (R_EAL r) * (M . B2) <= integral+ M,(max- f) )
assume A49: 0 < r ; :: thesis: (R_EAL r) * (M . B2) <= integral+ M,(max- f)
defpred S₁[ set ] means $1 in dom ((max- f) | B2);
deffunc H₁( set ) -> Element of ExtREAL = R_EAL r;
A50: for x being set st S₁[x] holds
H₁(x) in ExtREAL ;
consider g being PartFunc of X,ExtREAL such that
A51: ( ( 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(A50);
dom g = X /\ (dom ((max- f) | B2)) by A51, XBOOLE_0:def 4;
then A52: dom g = dom ((max- f) | B2) by XBOOLE_1:28;
dom ((max- f) | B2) = (dom (max- f)) /\ B2 by RELAT_1:90;
then A53: dom ((max- f) | B2) = B2 by A10, XBOOLE_1:28;
A54: g is_measurable_on B2

proof

dom (chi B2,X) = X by FUNCT_3:def 3;
then A55: B2 = (dom (chi B2,X)) /\ B2 by XBOOLE_1:28;
then A56: B2 = dom ((chi B2,X) | B2) by RELAT_1:90;
then A57: dom g = dom (r (#) ((chi B2,X) | B2)) by A52, A53, MESFUNC1:def 6;
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 A58: x in dom g ; :: thesis: g . x = (r (#) ((chi B2,X) | B2)) . x
then x in dom (r (#) ((chi B2,X) | B2)) by A52, A53, A56, MESFUNC1:def 6;
then A59: (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 A52, A53, A56, A58, FUNCT_1:70 ;
(chi B2,X) . x = 1 by A52, A53, A58, FUNCT_3:def 3;
then (r (#) ((chi B2,X) | B2)) . x = R_EAL r by A59, XXREAL_3:92;
hence g . x = (r (#) ((chi B2,X) | B2)) . x by A51, A58; :: thesis: verum

end;

then A60: g = r (#) ((chi B2,X) | B2) by A57, PARTFUN1:34;
(chi B2,X) | B2 is_measurable_on B2 by A55, Th48, MESFUNC2:32;
hence g is_measurable_on B2 by A56, A60, MESFUNC1:41; :: thesis: verum

end;

for x being set st x in dom g holds
0 <= g . x by A49, A51;
then A61: g is nonnegative by SUPINF_2:71;
A62: 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 A63: x in dom g ; :: thesis: g . x <= ((max- f) | B2) . x
then A64: ( x in dom f & f . x in {-infty } ) by A52, A53, FUNCT_1:def 13;
then A65: - (f . x) = +infty by TARSKI:def 1, XXREAL_3:5;
then A66: max (- (f . x)),0 = - (f . x) by XXREAL_0:def 10;
x in dom (max- f) by A64, MESFUNC2:def 3;
then (max- f) . x = +infty by A65, A66, MESFUNC2:def 3;
then ((max- f) | B2) . x = +infty by A52, A53, A63, FUNCT_1:72;
hence g . x <= ((max- f) | B2) . x by XXREAL_0:4; :: thesis: verum

end;

(max- f) | B2 is nonnegative by Lm1, Th21;
then integral+ M,g <= integral+ M,((max- f) | B2) by A15, A52, A53, A54, A61, A62, Th91;
then A67: integral+ M,g <= integral+ M,(max- f) by A16, XXREAL_0:2;
integral' M,g = (R_EAL r) * (M . (dom g)) by A49, A51, A52, A53, Th110;
hence (R_EAL r) * (M . B2) <= integral+ M,(max- f) by A52, A53, A61, A67, A51, Lm5, Th83; :: thesis: verum

end;

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

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

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

end;

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

(R_EAL 1) * (M . B2) <= integral+ M,(max- f) by A48;
then A71: 0 < integral+ M,(max- f) by A46, A47;
reconsider MB = M . B2 as Real by A47, A70, XXREAL_0:14;
reconsider I = integral+ M,(max- f) as Real by A2, A71, XXREAL_0:14;
A72: (R_EAL ((2 * I) / MB)) * (M . B2) <= integral+ M,(max- f) by A46, A47, A48, A71;
(R_EAL ((2 * I) / MB)) * (M . B2) = ((2 * I) / MB) * MB by EXTREAL1:13;
then 2 * I <= I by A46, A72, XCMPLX_1:88;
hence contradiction by A71, XREAL_1:157; :: thesis: verum

end;

end;

end;

thus (f " {+infty }) \/ (f " {-infty }) in S by A7, PROB_1:41; :: thesis: M . ((f " {+infty }) \/ (f " {-infty })) = 0
reconsider B1 = B1 as measure_zero of M by A17, MEASURE1:def 13;
thus M . ((f " {+infty }) \/ (f " {-infty })) = M . (B1 \/ B2)
.= 0 by A45, MEASURE1:71 ; :: thesis: verum