theorem :: FUNCT_4:77

for p, q being Function
for A being set st dom p c= A & dom q misses A holds
(p +* q) | A = p