let r be Real; :: thesis: for p being FinSequence of REAL st p is nonnegative & r >= 0 holds
r * p is nonnegative
let p be FinSequence of REAL ; :: thesis: ( p is nonnegative & r >= 0 implies r * p is nonnegative )
assume A1: ( p is nonnegative & r >= 0 ) ; :: thesis: r * p is nonnegative

now

let k be Element of NAT ; :: thesis: ( k in dom (r * p) implies (r * p) . k >= 0 )
assume A2: k in dom (r * p) ; :: thesis: (r * p) . k >= 0
k in dom p by A2, VALUED_1:def 5;
then A3: p . k >= 0 by A1, Def1;
(r * p) . k = r * (p . k) by RVSUM_1:66;
hence (r * p) . k >= 0 by A1, A3; :: thesis: verum

end;

hence r * p is nonnegative by Def1; :: thesis: verum