theorem :: MESFUN11:7

for X being non empty set
for f being PartFunc of X,ExtREAL
for r being positive Real holds less_dom (f,r) = less_dom ((max+ f),r) by Lm1;