theorem Th71: :: FUNCT_4:71

for p, q being Function
for A being set holds (p +* q) | A = (p | A) +* (q | A)