theorem Th23: :: FUNCT_4:23

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