theorem :: FUNCT_4:116
for f, g, h being Function st dom f misses dom h & f c= g +* h holds
f c= g