let x, A, X be set ; :: thesis: ( (chi (A,X)) . x = 1 implies x in A )
assume A1: (chi (A,X)) . x = 1 ; :: thesis: x in A

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 4; :: thesis: verum

end;

end;