:: deftheorem Def11 defines max- RFUNCT_3:def 11 :
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) ) ) );