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 Def4
.= - ((f . x) + (f . y)) by VECTSP_1:def 20
.= (- (f . x)) + (- (f . y)) by RLVECT_1:31
.= ((- f) . x) + (- (f . y)) by Def4
.= ((- f) . x) + ((- f) . y) by Def4 ; :: thesis: verum