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