let x be real number ; :: thesis: for f being real-valued FinSequence holds x * (- f) = - (x * f)
let f be real-valued FinSequence; :: thesis: x * (- f) = - (x * f)
thus x * (- f) = x * ((- 1) * f)
.= ((- 1) * x) * f by RVSUM_1:49
.= - (x * f) by RVSUM_1:49 ; :: thesis: verum