let f, g, h be Function; :: thesis: ( dom g = dom h implies (f +* g) +* h = f +* h )
assume A1: dom g = dom h ; :: thesis: (f +* g) +* h = f +* h
thus (f +* g) +* h = f +* (g +* h) by Th14
.= f +* h by A1, Th19 ; :: thesis: verum