theorem Th3: :: FINSEQ_4:3

for f being Function
for x being object holds
( f is_one-to-one_at x iff ( x in dom f & ( for z being object st z in dom f & x <> z holds
f . x <> f . z ) ) )