theorem Th29: :: MESFUN13:6

for X being non empty set
for f being PartFunc of X,ExtREAL
for x being Element of X holds
( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x )