:: deftheorem defines is_one-to-one_at FINSEQ_4:def 1 :
for f being Function
for x being object holds
( f is_one-to-one_at x iff f " (Im (f,x)) = {x} );