theorem :: GRFUNC_1:35
for X being set
for x being object
for f, g being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x