let f be FinSequence of REAL ; :: thesis: for i being Element of NAT st 1 <= i & i <= len f holds
( f . i >= f . (min_p f) & f . i >= min f )
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f implies ( f . i >= f . (min_p f) & f . i >= min f ) )
assume A1: ( 1 <= i & i <= len f ) ; :: thesis: ( f . i >= f . (min_p f) & f . i >= min f )
then A2: i in dom f by FINSEQ_3:27;
hence f . i >= f . (min_p f) by A1, Def2; :: thesis: f . i >= min f
thus f . i >= min f by A1, A2, Def2; :: thesis: verum