theorem Th23: :: MESFUN11:23

for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is without-infty & f is without+infty holds
( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) & dom (g - f) = (dom f) /\ (dom g) )