:: deftheorem Def3 defines max- MESFUNC2:def 3 :
for C being non empty set
for f, b₃ being PartFunc of C,ExtREAL holds
( b₃ = max- f iff ( dom b₃ = dom f & ( for x being Element of C st x in dom b₃ holds
b₃ . x = max ((- (f . x)),0.) ) ) );