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

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