let R, S be AbGroup; :: thesis: for f being Homomorphism of R,S holds 0. S in rng f
let f be Homomorphism of R,S; :: thesis: 0. S in rng f
A1: f . (0. R) = 0. S by MOD_4:40;
dom f = the carrier of R by FUNCT_2:def 1;
hence 0. S in rng f by A1, FUNCT_1:def 3; :: thesis: verum