for X1, X2 being set
for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds
X1 c= X2