theorem :: FUNCT_4:106

for z being object
for f being Function
for x, y being object st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y