theorem Th30: :: FUNCT_7:31

for f being Function
for d, i being object st i in dom f holds
(f +* (i,d)) . i = d