let f be Function; :: thesis: for x being object holds
( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) )
let x be object ; :: thesis: ( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) )
thus ( f is_one-to-one_at x implies ( x in dom f & f " {(f . x)} = {x} ) ) :: thesis: ( x in dom f & f " {(f . x)} = {x} implies f is_one-to-one_at x )

proof

assume A1: f is_one-to-one_at x ; :: thesis: ( x in dom f & f " {(f . x)} = {x} )
hence A2: x in dom f by Th1; :: thesis: f " {(f . x)} = {x}
f " (Im (f,x)) = {x} by A1;
hence f " {(f . x)} = {x} by A2, FUNCT_1:59; :: thesis: verum

end;

assume ( x in dom f & f " {(f . x)} = {x} ) ; :: thesis: f is_one-to-one_at x
hence f " (Im (f,x)) = {x} by FUNCT_1:59; :: according to FINSEQ_4:def 1 :: thesis: verum