let A, X be set ; :: thesis: for B being Subset of X holds dom ((chi (A,X)) | B) = B
let B be Subset of X; :: thesis: dom ((chi (A,X)) | B) = B
dom ((chi (A,X)) | B) = (dom (chi (A,X))) /\ B by RELAT_1:61
.= X /\ B by FUNCT_2:def 1 ;
hence dom ((chi (A,X)) | B) = B by XBOOLE_1:28; :: thesis: verum