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