let A, X be set ; rng (chi (A,X)) c= {0,1}
let y be object ; TARSKI:def 3 ( not y in rng (chi (A,X)) or y in {0,1} )
assume
y in rng (chi (A,X))
; y in {0,1}
then consider x being object such that
A1:
x in dom (chi (A,X))
and
A2:
y = (chi (A,X)) . x
by FUNCT_1:def 3;
A3:
( x in A or not x in A )
;
x in X
by A1, Def3;
then
( y = {} or y = 1 )
by A2, A3, Def3;
hence
y in {0,1}
by TARSKI:def 2; verum