for f being FinSequence of REAL
for a being Real st len f > 0 & a > 0 holds
( max (a * f) = a * (max f) & max_p (a * f) = max_p f )