theorem :: FUNCT_4:93

for f, g being Function holds (f +* g) +* g = f +* g ;