let f be Function; :: thesis: for x being object st f is_one-to-one_at x holds
x in dom f
let x be object ; :: thesis: ( f is_one-to-one_at x implies x in dom f )
assume f is_one-to-one_at x ; :: thesis: x in dom f
then f " (Im (f,x)) = {x} ;
then x in f " (Im (f,x)) by TARSKI:def 1;
hence x in dom f by FUNCT_1:def 7; :: thesis: verum