for a, b, c, d being set
for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds
(a,c) --> (b,d) c= f