theorem SFG: :: RVSUM_4:5
for f, g being complex-valued Function
for X being set holds (f + g) | X = (f | X) + (g | X)