let g, h, f be Function; :: thesis: ( dom g misses dom h implies ((f +* g) +* h) +* g = (f +* g) +* h )
assume Z: dom g misses dom h ; :: thesis: ((f +* g) +* h) +* g = (f +* g) +* h
thus ((f +* g) +* h) +* g = (f +* (g +* h)) +* g by Th15
.= f +* ((g +* h) +* g) by Th15
.= f +* ((h +* g) +* g) by Z, Th36
.= f +* (h +* g) by Th99
.= f +* (g +* h) by Z, Th36
.= (f +* g) +* h by Th15 ; :: thesis: verum