theorem Th38: :: MESFUN7C:38

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