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

now

thus A1: dom f = X by FUNCT_2:def 1; :: thesis: for x being set st x in X holds
( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) )
let x be set ; :: 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 13;
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} & f . x in rng f & rng f c= {{} ,1} ) by A1, A2, FUNCT_1:def 5, FUNCT_1:def 13, RELAT_1:def 19;
then ( f . x <> 1 & f . x in {{} ,1} ) by TARSKI:def 1;
hence f . x = {} by TARSKI:def 2; :: thesis: verum

end;

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