let F be FinSequence of INT ; :: thesis: for m being Element of NAT st 1 <= m & m <= len F holds
min_at (F,m,m) = m
let m be Element of 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 Element of NAT st m <= i & i < m holds
F . m < F . i ;
for i being Element of 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, Th63; :: thesis: verum