for R being Relation
for f being Function st dom f c= dom R & R c= f holds
R = f by Lm42;