theorem Th59: :: FINSEQ_6:161

for F being FinSequence of INT
for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds
( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) ) )