let f, g be Function; :: thesis: (f +* g) +* g = f +* g
thus (f +* g) +* g = f +* (g +* g) by Th15
.= f +* g ; :: thesis: verum