for x, y being set
for f being Function st ( x in dom f implies ( y in dom f & f . x = f . y ) ) holds
f = f * ((id (dom f)) +* (x,y))