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 that
A1: p is nonnegative and
A2: r >= 0 ; :: thesis: r * p is nonnegative

now :: thesis: for k being Nat st k in dom (r * p) holds
(r * p) . k >= 0

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

end;

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