let X be non empty set ; :: thesis: for A being non empty Subset of X
for B being set st B meets dom (chi A,A) holds
rng ((chi A,A) | B) = {1}
let A be non empty Subset of X; :: thesis: for B being set st B meets dom (chi A,A) holds
rng ((chi A,A) | B) = {1}
let B be set ; :: thesis: ( B meets dom (chi A,A) implies rng ((chi A,A) | B) = {1} )
assume A1: B /\ (dom (chi A,A)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: rng ((chi A,A) | B) = {1}
rng ((chi A,A) | B) c= rng (chi A,A) by RELAT_1:99;
then A2: rng ((chi A,A) | B) c= {1} by Th19;
rng ((chi A,A) | B) <> {}

proof

dom ((chi A,A) | B) = B /\ (dom (chi A,A)) by RELAT_1:90;
hence rng ((chi A,A) | B) <> {} by A1, RELAT_1:65; :: thesis: verum

end;

hence rng ((chi A,A) | B) = {1} by A2, ZFMISC_1:39; :: thesis: verum