let X be non empty set ; :: thesis: for S being SigmaField of X
for A, B being Element of S holds Xchi (A,X) is B -measurable
let S be SigmaField of X; :: thesis: for A, B being Element of S holds Xchi (A,X) is B -measurable
let A, B be Element of S; :: thesis: Xchi (A,X) is B -measurable
A1: dom (Xchi (A,X)) = X by FUNCT_2:def 1;
for r being Real holds B /\ (great_eq_dom ((Xchi (A,X)),r)) in S

proof

let r be Real; :: thesis: B /\ (great_eq_dom ((Xchi (A,X)),r)) in S

per cases ( r > 0 or r <= 0 ) ;

suppose r > 0 ; :: thesis: B /\ (great_eq_dom ((Xchi (A,X)),r)) in S

then B /\ (great_eq_dom ((Xchi (A,X)),r)) = B /\ A by Lm08;
hence B /\ (great_eq_dom ((Xchi (A,X)),r)) in S ; :: thesis: verum

end;

suppose r <= 0 ; :: thesis: B /\ (great_eq_dom ((Xchi (A,X)),r)) in S

then great_eq_dom ((Xchi (A,X)),r) = X by Lm09;
then B /\ (great_eq_dom ((Xchi (A,X)),r)) = B by XBOOLE_1:28;
hence B /\ (great_eq_dom ((Xchi (A,X)),r)) in S ; :: thesis: verum

end;

end;

end;

hence Xchi (A,X) is B -measurable by A1, MESFUNC1:27; :: thesis: verum