let X be non empty set ; :: thesis: for S being SigmaField of X
for A, B being Element of S
for er being ExtReal holds chi (er,A,X) is B -measurable
let S be SigmaField of X; :: thesis: for A, B being Element of S
for er being ExtReal holds chi (er,A,X) is B -measurable
let A, B be Element of S; :: thesis: for er being ExtReal holds chi (er,A,X) is B -measurable
let er be ExtReal; :: thesis: chi (er,A,X) is B -measurable
a1: Xchi (A,X) is B -measurable 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 B -measurable

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

end;

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

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

end;

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

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 B -measurable by a3, MESFUNC1:37, MESFUNC2:29; :: thesis: verum

end;

end;