let f be FinSequence of ExtREAL ; :: thesis: for i being Nat st 1 <= i & i <= len f holds
( f . i <= f . (max_p f) & f . i <= max f )
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies ( f . i <= f . (max_p f) & f . i <= max f ) )
assume A1: ( 1 <= i & i <= len f ) ; :: thesis: ( f . i <= f . (max_p f) & f . i <= max f )
then A2: i in dom f by FINSEQ_3:25;
hence f . i <= f . (max_p f) by A1, Def1; :: thesis: f . i <= max f
thus f . i <= max f by A1, A2, Def1; :: thesis: verum