theorem Th19: :: MESFUNC7:19

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