theorem :: FUNCT_7:106
for f, g, h being Function holds
( f +* h = g +* h iff f,g equal_outside dom h )