let x be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for r being Scalar of holds (- f) . (r * x) = r * ((- f) . x)
let r be Scalar of ; :: thesis: (- f) . (r * x) = r * ((- f) . x)
thus (- f) . (r * x) = - (f . (r * x)) by Def4
.= - (r * (f . x)) by Def8
.= r * (- (f . x)) by Lm1
.= r * ((- f) . x) by Def4 ; :: thesis: verum