let H, G be AddGroup; :: thesis: for f being Homomorphism of G,H
for x being Element of G holds f . (- x) = - (f . x)
let f be Homomorphism of G,H; :: thesis: for x being Element of G holds f . (- x) = - (f . x)
let x be Element of G; :: thesis: f . (- x) = - (f . x)
set a = 0. G;
set b = 0. H;
set y = f . x;
x + (- x) = 0. G by RLVECT_1:def 13;
then (f . x) + (f . (- x)) = f . (0. G) by Def19
.= 0. H by Lm15 ;
hence f . (- x) = - (f . x) by VECTSP_1:63; :: thesis: verum