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