theorem Th24: :: FUNCT_4:24

for f, g being Function holds (f +* g) | ((dom f) \ (dom g)) c= f