for X being set
for f being Function of X,X st f is one-to-one holds
for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 by Th55;