theorem Th21: :: GRFUNC_1:23

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