for f being FinSequence of REAL
for n being Nat st n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )