let f be FinSequence of REAL ; :: thesis: for i being Element of NAT st 1 <= i & i <= len f holds
( f . i <= f . (max_p f) & f . i <= max f )
let i be Element of 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:27;
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