f:A->B is one-to-one if f(x)=f(y) implies x=y or, equivalently, if x not = y implies f(x) not = f(y).
