theorem Th2: :: FINSEQ_4:2

for f being Function
for x being object holds
( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) )