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