:: deftheorem Def1 defines max_p MEASUR12:def 1 :
for f being FinSequence of ExtREAL
for b₂ being Nat holds
( b₂ = max_p f iff ( ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat st i in dom f holds
f . i <= f . b₂ ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) ) );