theorem :: GRFUNC_1:31
for f, g being Function
for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}