for X being non empty set
for Y being set
for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )