let X be set ; :: thesis: for C being non empty set
for c being Element of C holds
( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
let C be non empty set ; :: thesis: for c being Element of C holds
( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
let c be Element of C; :: thesis: ( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
thus ( (chi (X,C)) . c <> 1 implies (chi (X,C)) . c = 0 ) :: thesis: ( (chi (X,C)) . c = 0 implies (chi (X,C)) . c <> 1 )

proof

c in C ;
then c in dom (chi (X,C)) by Th77;
then A1: (chi (X,C)) . c in rng (chi (X,C)) by FUNCT_1:def 3;
A2: rng (chi (X,C)) c= {0,1} by FUNCT_3:39;
assume (chi (X,C)) . c <> 1 ; :: thesis: (chi (X,C)) . c = 0
hence (chi (X,C)) . c = 0 by A1, A2, TARSKI:def 2; :: thesis: verum

end;

assume that
A3: (chi (X,C)) . c = 0 and
A4: (chi (X,C)) . c = 1 ; :: thesis: contradiction
thus contradiction by A3, A4; :: thesis: verum