thus (f +* g) +* g = f +* (g +* g) by Th14
.= f +* g ; :: thesis: verum