let x, A, X be set ; :: thesis: ( x in X \ A implies (chi (A,X)) . x = 0 )
assume A1: x in X \ A ; :: thesis: (chi (A,X)) . x = 0
then not x in A by XBOOLE_0:def 5;
hence (chi (A,X)) . x = 0 by A1, Def3; :: thesis: verum