theorem Th9: :: FINSEQ_4:9

for f being Function
for x being object holds
( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )