for f being Function holds
( ( for x being object st x in dom f holds
f is_one-to-one_at x ) iff f is one-to-one )