let X be non empty set ; 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; for B being set st B meets dom (chi (A,A)) holds
rng ((chi (A,A)) | B) = {1}
let B be set ; ( 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))) <> {}
; XBOOLE_0:def 7 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; verum