:: deftheorem Def10 defines max+ RFUNCT_3:def 10 :
for D being non empty set
for F, b₃ being PartFunc of D,REAL holds
( b₃ = max+ F iff ( dom b₃ = dom F & ( for d being Element of D st d in dom b₃ holds
b₃ . d = max+ (F . d) ) ) );