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