theorem Th39: :: MESFUN7C:39

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