theorem :: MESFUN11:31

for X being non empty set
for f being nonnegative PartFunc of X,ExtREAL holds f = max+ f