theorem :: RFINSEQ2:10

for f being real-valued FinSequence
for a being Real st len f > 0 & a > 0 holds
( min (a * f) = a * (min f) & min_p (a * f) = min_p f )