let x, y be Vector of V; :: according to VECTSP_1:def 19 :: thesis: (- f) . (x + y) = ((- f) . x) + ((- f) . y)
thus (- f) . (x + y) = - (f . (x + y)) by HDef4
.= - ((f . x) + (f . y)) by VECTSP_1:def 20
.= (- (f . x)) + (- (f . y))
.= ((- f) . x) + (- (f . y)) by HDef4
.= ((- f) . x) + ((- f) . y) by HDef4 ; :: thesis: verum