let G, H 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 10;
then (f . x) + (f . (- x)) = f . (0. G) by VECTSP_1:def 20
.= 0. H by Lm13 ;
hence f . (- x) = - (f . x) by VECTSP_1:16; :: thesis: verum