theorem :: FUNCT_7:34

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