let G, H be AddGroup; :: thesis: for f being Homomorphism of G,H holds f . (0. G) = 0. H

let f be Homomorphism of G,H; :: thesis: f . (0. G) = 0. H

set a = 0. G;

(0. G) + (0. G) = 0. G by RLVECT_1:def 4;

then (f . (0. G)) + (f . (0. G)) = f . (0. G) by VECTSP_1:def 20

.= (f . (0. G)) + (0. H) by RLVECT_1:def 4 ;

hence f . (0. G) = 0. H by RLVECT_1:8; :: thesis: verum

let f be Homomorphism of G,H; :: thesis: f . (0. G) = 0. H

set a = 0. G;

(0. G) + (0. G) = 0. G by RLVECT_1:def 4;

then (f . (0. G)) + (f . (0. G)) = f . (0. G) by VECTSP_1:def 20

.= (f . (0. G)) + (0. H) by RLVECT_1:def 4 ;

hence f . (0. G) = 0. H by RLVECT_1:8; :: thesis: verum