theorem :: RFINSEQ2:4

for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( min_p f = 1 & min f = r )