theorem Th34: :: FUNCT_7:35

for f being Function
for i being set holds f +* (i,(f . i)) = f