for F being FinSequence of INT
for m being Nat st 1 <= m & m <= len F holds
min_at (F,m,m) = m