let F be FinSequence of INT ; :: thesis: for m being Nat st 1 <= m & m <= len F holds
min_at (F,m,m) = m
let m be Nat; :: thesis: ( 1 <= m & m <= len F implies min_at (F,m,m) = m )
assume that
A1: 1 <= m and
A2: m <= len F ; :: thesis: min_at (F,m,m) = m
A3: for i being Nat st m <= i & i < m holds
F . m < F . i ;
for i being Nat st m <= i & i <= m holds
F . m <= F . i by XXREAL_0:1;
hence min_at (F,m,m) = m by A1, A2, A3, Th59; :: thesis: verum