let f be FinSequence of ExtREAL ; :: thesis: for i being Nat st 1 <= i & i <= len f holds
( f . i >= f . (min_p f) & f . i >= min f )
let i be 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:25;
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