let x, y be Vector of V; :: according to HAHNBAN1:def 11 :: thesis: (- f) . (x + y) = ((- f) . x) + ((- f) . y)
thus (- f) . (x + y) = - (f . (x + y)) by Def7
.= - ((f . x) + (f . y)) by Def11
.= (- (f . x)) + (- (f . y)) by RLVECT_1:45
.= ((- f) . x) + (- (f . y)) by Def7
.= ((- f) . x) + ((- f) . y) by Def7 ; :: thesis: verum