let A, X be set ; :: thesis: for x being object st (chi (A,X)) . x = 1 holds
x in A
let x be object ; :: thesis: ( (chi (A,X)) . x = 1 implies x in A )
assume A1: (chi (A,X)) . x = 1 ; :: thesis: x in A
A2: 1 = succ 0
.= {0} ;

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: x in A

hence x in A by A1, Def3; :: thesis: verum

end;

suppose not x in X ; :: thesis: x in A

then not x in dom (chi (A,X)) by Def3;
hence x in A by A1, FUNCT_1:def 2, A2; :: thesis: verum

end;

end;