let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)
let M be sigma_Measure of S; :: thesis: for E being Element of S
for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)
let E be Element of S; :: thesis: for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)
let er be ExtReal; :: thesis: Integral (M,((chi (er,E,X)) | E)) = er * (M . E)
reconsider XX = X as Element of S by MEASURE1:7;
A1: XX = dom (chi (er,E,X)) by FUNCT_2:def 1;
then dom ((chi (er,E,X)) | (XX \ E)) = XX /\ (XX \ E) by RELAT_1:61;
then A2: dom ((chi (er,E,X)) | (XX \ E)) = XX \ E by XBOOLE_1:28;
A3: (chi (er,E,X)) | (XX \ E) is XX \ E -measurable by Th15;
A4: E \/ (XX \ E) = X \/ E by XBOOLE_1:39
.= X by XBOOLE_1:12 ;
A5: E misses XX \ E by XBOOLE_1:79;
A6: Integral (M,(chi (er,E,X))) = Integral (M,((chi (er,E,X)) | X)) ;

per cases ( er = +infty or er = -infty or ( er <> +infty & er <> -infty ) ) ;

suppose er = +infty ; :: thesis: Integral (M,((chi (er,E,X)) | E)) = er * (M . E)

then A7: chi (er,E,X) = Xchi (E,X) by Th2;
then A8: (chi (er,E,X)) | (XX \ E) is nonnegative by MESFUNC5:15;
chi (er,E,X) is XX -measurable by Th13;
then V: ex W being Element of S st
( W = dom (chi (er,E,X)) & chi (er,E,X) is W -measurable ) by A1;
Integral (M,(chi (er,E,X))) = (Integral (M,((chi (er,E,X)) | E))) + (Integral (M,((chi (er,E,X)) | (XX \ E)))) by A4, V, A5, A6, A7, MESFUNC5:91;
then A9: (Integral (M,((chi (er,E,X)) | E))) + (Integral (M,((chi (er,E,X)) | (XX \ E)))) = er * (M . E) by Th49;
for x being Element of X st x in dom ((chi (er,E,X)) | (XX \ E)) holds
((chi (er,E,X)) | (XX \ E)) . x = 0 by A5, Th16;
then integral+ (M,((chi (er,E,X)) | (XX \ E))) = 0 by A2, Th15, MESFUNC5:87;
then Integral (M,((chi (er,E,X)) | (XX \ E))) = 0 by A2, A8, Th15, MESFUNC5:88;
hence Integral (M,((chi (er,E,X)) | E)) = er * (M . E) by A9, XXREAL_3:4; :: thesis: verum

end;

suppose er = -infty ; :: thesis: Integral (M,((chi (er,E,X)) | E)) = er * (M . E)

then A10: chi (er,E,X) = - (Xchi (E,X)) by Th2;
then A11: (chi (er,E,X)) | (XX \ E) is nonpositive by MESFUN11:1;
chi (er,E,X) is XX -measurable by Th13;
then ex W being Element of S st
( W = dom (chi (er,E,X)) & chi (er,E,X) is W -measurable ) by A1;
then Integral (M,(chi (er,E,X))) = (Integral (M,((chi (er,E,X)) | E))) + (Integral (M,((chi (er,E,X)) | (XX \ E)))) by A4, A5, A6, A10, MESFUN11:62;
then A12: (Integral (M,((chi (er,E,X)) | E))) + (Integral (M,((chi (er,E,X)) | (XX \ E)))) = er * (M . E) by Th49;
A13: dom ((- (chi (er,E,X))) | (XX \ E)) = dom (- ((chi (er,E,X)) | (XX \ E))) by MESFUN11:3
.= XX \ E by A2, MESFUNC1:def 7 ;
- ((chi (er,E,X)) | (XX \ E)) is XX \ E -measurable by A2, Th15, MEASUR11:63;
then A14: (- (chi (er,E,X))) | (XX \ E) is XX \ E -measurable by MESFUN11:3;

now :: thesis: for x being Element of X st x in dom ((- (chi (er,E,X))) | (XX \ E)) holds
((- (chi (er,E,X))) | (XX \ E)) . x = 0

let x be Element of X; :: thesis: ( x in dom ((- (chi (er,E,X))) | (XX \ E)) implies ((- (chi (er,E,X))) | (XX \ E)) . x = 0 )
assume A15: x in dom ((- (chi (er,E,X))) | (XX \ E)) ; :: thesis: ((- (chi (er,E,X))) | (XX \ E)) . x = 0
then x in (dom (- (chi (er,E,X)))) /\ (XX \ E) by RELAT_1:61;
then A16: ( x in dom (- (chi (er,E,X))) & x in XX \ E ) by XBOOLE_0:def 4;
then ( x in X & not x in E ) by XBOOLE_0:def 5;
then (chi (er,E,X)) . x = 0 by Def1;
then (- (chi (er,E,X))) . x = - 0 by A16, MESFUNC1:def 7;
hence ((- (chi (er,E,X))) | (XX \ E)) . x = 0 by A15, FUNCT_1:47; :: thesis: verum

end;

then integral+ (M,((- (chi (er,E,X))) | (XX \ E))) = 0 by A13, A14, MESFUNC5:87;
then integral+ (M,(- ((chi (er,E,X)) | (XX \ E)))) = 0 by MESFUN11:3;
then Integral (M,((chi (er,E,X)) | (XX \ E))) = - 0 by A2, A3, A11, MESFUN11:57;
hence Integral (M,((chi (er,E,X)) | E)) = er * (M . E) by A12, XXREAL_3:4; :: thesis: verum

end;

suppose ( er <> +infty & er <> -infty ) ; :: thesis: Integral (M,((chi (er,E,X)) | E)) = er * (M . E)

then er in REAL by XXREAL_0:14;
then reconsider r = er as Real ;
chi (er,E,X) = r (#) (chi (E,X)) by Th1;
then A17: (chi (er,E,X)) | E = r (#) ((chi (E,X)) | E) by MESFUN11:2;
A18: (chi (E,X)) | E is nonnegative by MESFUNC5:15;
A19: (chi (E,X)) | E is_simple_func_in S by Th12, MESFUNC5:34;
hence Integral (M,((chi (er,E,X)) | E)) = r * (integral' (M,((chi (E,X)) | E))) by A17, MESFUNC5:15, MESFUN11:59
.= r * (Integral (M,((chi (E,X)) | E))) by A19, A18, MESFUNC5:89
.= er * (M . E) by MESFUNC9:14 ;
:: thesis: verum

end;

end;