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

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