for X being set
for Y being non empty set
for p being Function of X,Y st p is one-to-one holds
for x1, x2 being Subset of X st x1 <> x2 holds
p .: x1 <> p .: x2