let x be Vector of V; :: according to ZMODLAT1:def 22 :: 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 HDef4
.= - (r * (f . x)) by HDef8
.= r * (- (f . x))
.= r * ((- f) . x) by HDef4 ; :: thesis: verum