for r being Real
for p being FinSequence of REAL st p is nonnegative & r >= 0 holds
r * p is nonnegative