theorem Th21: :: MESFUNC7:21

for X being non empty set
for f, g being PartFunc of X,ExtREAL
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x