theorem :: FUNCT_4:115

for f, g, h being Function st dom g misses dom h holds
((f +* g) +* h) +* g = (f +* g) +* h