for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
for x being Element of X
for A being Subset of X st f . x in f .: A holds
x in A