let X be non empty set ; 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; for A, B being Element of S holds Xchi (A,X) is B -measurable
let A, B be Element of S; 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
hence
Xchi (A,X) is B -measurable
by A1, MESFUNC1:27; verum