theorem :: GRFUNC_1:33

for f, g, h being Function st f c= g & f c= h holds
g | (dom f) = h | (dom f)