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))) = 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))) = 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))) = er * (M . E)
let E be Element of S; :: thesis: for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)
let er be ExtReal; :: thesis: Integral (M,(chi (er,E,X))) = er * (M . E)
reconsider XX = X as Element of S by MEASURE1:7;

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

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

then a2: chi (er,E,X) = Xchi (E,X) by Th2;

per cases ( M . E <> 0 or M . E = 0 ) ;

suppose a3: M . E <> 0 ; :: thesis: Integral (M,(chi (er,E,X))) = er * (M . E)

then a4: M . E > 0 by MEASURE1:def 2;
thus Integral (M,(chi (er,E,X))) = +infty by a2, a3, MEASUR10:33
.= er * (M . E) by a1, a4, XXREAL_3:def 5 ; :: thesis: verum

end;

suppose a5: M . E = 0 ; :: thesis: Integral (M,(chi (er,E,X))) = er * (M . E)

then Integral (M,(chi (er,E,X))) = 0 by a2, MEASUR10:33;
hence Integral (M,(chi (er,E,X))) = er * (M . E) by a5; :: thesis: verum

end;

end;

end;

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

then a7: chi (er,E,X) = - (Xchi (E,X)) by Th2;
a10: dom (Xchi (E,X)) = XX by FUNCT_2:def 1;
W: Xchi (E,X) is XX -measurable by MEASUR10:32;

per cases ( M . E <> 0 or M . E = 0 ) ;

suppose a8: M . E <> 0 ; :: thesis: Integral (M,(chi (er,E,X))) = er * (M . E)

then a9: M . E > 0 by MEASURE1:def 2;
thus Integral (M,(chi (er,E,X))) = - (Integral (M,(Xchi (E,X)))) by a10, a7, MESFUN11:52, W
.= - +infty by a8, MEASUR10:33
.= er * (M . E) by a6, a9, XXREAL_3:def 5, XXREAL_3:6 ; :: thesis: verum

end;

suppose a12: M . E = 0 ; :: thesis: Integral (M,(chi (er,E,X))) = er * (M . E)

thus Integral (M,(chi (er,E,X))) = - (Integral (M,(Xchi (E,X)))) by a10, a7, MESFUN11:52, W
.= - 0 by a12, MEASUR10:33
.= er * (M . E) by a12 ; :: thesis: verum

end;

end;

end;

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

then er in REAL by XXREAL_0:14;
then reconsider r = er as Real ;
a14: chi (E,X) is_simple_func_in S by Th12;
chi (er,E,X) = r (#) (chi (E,X)) by Th1;
hence Integral (M,(chi (er,E,X))) = r * (integral' (M,(chi (E,X)))) by Th12, MESFUN11:59
.= r * (Integral (M,(chi (E,X)))) by a14, MESFUNC5:89
.= er * (M . E) by MESFUNC9:14 ;
:: thesis: verum

end;

end;