theorem Th2: :: RFINSEQ2:2

for f being real-valued FinSequence
for i being Nat st 1 <= i & i <= len f holds
( f . i >= f . (min_p f) & f . i >= min f )