theorem :: YELLOW20:45

for f, g being Function st dom f is Relation & ~ f c= ~ g holds
f c= g