theorem :: FUNCT_4:107

for f being Function
for x, y being object st not x in dom f holds
f c= f +* (x .--> y)