theorem Th27: :: GRFUNC_1:29

for f, g being Function
for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}