theorem :: FUNCT_1:89

for f being Function holds
( f is one-to-one iff for y being object ex x being object st f " {y} c= {x} )