let X be set ; :: thesis: for f being Function of X,{0,1} holds f = chi ((f " {1}),X)
let f be Function of X,{0,1}; :: thesis: f = chi ((f " {1}),X)

now :: thesis: ( dom f = X & ( for x being object st x in X holds
( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) ) ) )

thus A1: dom f = X by FUNCT_2:def 1; :: thesis: for x being object st x in X holds
( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) )
let x be object ; :: thesis: ( x in X implies ( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) ) )
assume A2: x in X ; :: thesis: ( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) )
thus ( x in f " {1} implies f . x = 1 ) :: thesis: ( not x in f " {1} implies f . x = {} )

proof

assume x in f " {1} ; :: thesis: f . x = 1
then f . x in {1} by FUNCT_1:def 7;
hence f . x = 1 by TARSKI:def 1; :: thesis: verum

end;

assume not x in f " {1} ; :: thesis: f . x = {}
then not f . x in {1} by A1, A2, FUNCT_1:def 7;
then A3: ( rng f c= {{},1} & f . x <> 1 ) by RELAT_1:def 19, TARSKI:def 1;
f . x in rng f by A1, A2, FUNCT_1:def 3;
hence f . x = {} by A3, TARSKI:def 2; :: thesis: verum

end;

hence f = chi ((f " {1}),X) by Def3; :: thesis: verum