theorem :: FUNCT_4:78

for f being Function
for A, B being set holds f | (A \/ B) = (f | A) +* (f | B)