for f being FinSequence of REAL
for i being Nat st 1 <= i & i <= len f holds
( f . i <= f . (max_p f) & f . i <= max f )