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 5;
A2: rng (chi X,C) c= {0 ,1} by FUNCT_3:48;
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