theorem :: FUNCT_7:117

for f, g being Function
for x, y being object holds (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))