let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let er be ExtReal; :: thesis:
reconsider XX = X as Element of S by MEASURE1:7;

per cases ;

suppose a1: er = +infty ; :: thesis:

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

per cases ;

suppose a3: M . E <> 0 ; :: thesis:

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:

end;

suppose a5: M . E = 0 ; :: thesis:

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:

end;

end;

end;

suppose a6: er = -infty ; :: thesis:

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 ;

suppose a8: M . E <> 0 ; :: thesis:

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:

end;

suppose a12: M . E = 0 ; :: thesis:

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:

end;

end;

end;

suppose ( er <> +infty & er <> -infty ) ; :: thesis:

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:

end;

end;