theorem Th23: :: MESFUN11:23

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