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} )
A1: dom ((chi (A,A)) | B) = B /\ (dom (chi (A,A))) by RELAT_1:61;
rng ((chi (A,A)) | B) c= rng (chi (A,A)) by RELAT_1:70;
then A2: rng ((chi (A,A)) | B) c= {1} by Th15;
assume B /\ (dom (chi (A,A))) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: rng ((chi (A,A)) | B) = {1}
then rng ((chi (A,A)) | B) <> {} by A1, RELAT_1:42;
hence rng ((chi (A,A)) | B) = {1} by A2, ZFMISC_1:33; :: thesis: verum