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 A1: ( 1 <= m & m <= len F ) ; :: thesis: min_at F,m,m = m
A2: for i being Element of NAT st m <= i & i <= m holds
F . m <= F . i by XXREAL_0:1;
for i being Element of NAT st m <= i & i < m holds
F . m < F . i ;
hence min_at F,m,m = m by A1, A2, Th63; :: thesis: verum