let X, Y be set ; :: thesis: ( X misses Y implies for x being Element of X holds (chi (Y,X)) . x = 0 )
assume A1: X misses Y ; :: thesis: for x being Element of X holds (chi (Y,X)) . x = 0
let x be Element of X; :: thesis: (chi (Y,X)) . x = 0

per cases ( not X is empty or X is empty ) ;

suppose A2: not X is empty ; :: thesis: (chi (Y,X)) . x = 0

then not x in Y by A1, XBOOLE_0:def 4;
then x in X \ Y by A2, XBOOLE_0:def 5;
hence (chi (Y,X)) . x = 0 by FUNCT_3:37; :: thesis: verum

end;

suppose X is empty ; :: thesis: (chi (Y,X)) . x = 0

hence (chi (Y,X)) . x = 0 ; :: thesis: verum

end;

end;