theorem Th1: :: RFINSEQ2:1

for f being real-valued FinSequence
for i being Nat st 1 <= i & i <= len f holds
( f . i <= f . (max_p f) & f . i <= max f )