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