theorem Th16: :: MESFUNC5:16

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