theorem Th3: :: AMI_8:3

for f, g being Function
for w, x, y, z being object st dom f = dom g & f . w = g . w & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {w,x,y,z} = g | {w,x,y,z}