theorem :: FUNCT_2:19

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
( f is one-to-one iff for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )