let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S
for er being ExtReal holds chi (er,A,X) is_measurable_on B
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A, B being Element of S
for er being ExtReal holds chi (er,A,X) is_measurable_on B
let M be sigma_Measure of S; :: thesis: for A, B being Element of S
for er being ExtReal holds chi (er,A,X) is_measurable_on B
let A, B be Element of S; :: thesis: for er being ExtReal holds chi (er,A,X) is_measurable_on B
let er be ExtReal; :: thesis: chi (er,A,X) is_measurable_on B
a1: Xchi (A,X) is_measurable_on B by MEASUR10:32;
a2: dom (Xchi (A,X)) = X by FUNCT_2:def 1;

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

suppose er = +infty ; :: thesis: chi (er,A,X) is_measurable_on B

hence chi (er,A,X) is_measurable_on B by a1, Th2; :: thesis: verum

end;

suppose er = -infty ; :: thesis: chi (er,A,X) is_measurable_on B

then chi (er,A,X) = - (Xchi (A,X)) by Th2;
hence chi (er,A,X) is_measurable_on B by a2, MEASUR10:32, MEASUR11:63; :: thesis: verum

end;

suppose ( er <> +infty & er <> -infty ) ; :: thesis: chi (er,A,X) is_measurable_on B

then er in REAL by XXREAL_0:14;
then reconsider r = er as Real ;
a3: chi (er,A,X) = r (#) (chi (A,X)) by Th1;
dom (chi (A,X)) = X by FUNCT_3:def 3;
hence chi (er,A,X) is_measurable_on B by a3, MESFUNC1:37, MESFUNC2:29; :: thesis: verum

end;

end;