theorem :: FUNCT_4:16

for x being object
for f, g being Function st dom f misses dom g & x in dom f holds
(f +* g) . x = f . x