theorem :: RFINSEQ2:3

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