let f be Function; :: thesis: for x being set holds
( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )
let x be set ; :: thesis: ( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )
thus ( f is_one-to-one_at x implies ( x in dom f & f just_once_values f . x ) ) :: thesis: ( x in dom f & f just_once_values f . 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 just_once_values f . x )
hence x in dom f by Th2; :: thesis: f just_once_values f . x
{x} = f " {(f . x)} by A1, Th3;
hence f just_once_values f . x by Th8; :: thesis: verum

end;

assume that
A2: x in dom f and
A3: f just_once_values f . x ; :: thesis: f is_one-to-one_at x
consider z being set such that
A4: f " {(f . x)} = {z} by A3, Th8;
f . x in {(f . x)} by TARSKI:def 1;
then x in {z} by A2, A4, FUNCT_1:def 7;
then x = z by TARSKI:def 1;
hence f is_one-to-one_at x by A2, A4, Th3; :: thesis: verum