let G, H be Group; :: thesis: for g being Homomorphism of G,H holds rng g = the carrier of (Image g)
let g be Homomorphism of G,H; :: thesis: rng g = the carrier of (Image g)
the carrier of (Image g) = g .: the carrier of G by Def10
.= g .: (dom g) by FUNCT_2:def 1
.= rng g by RELAT_1:113 ;
hence rng g = the carrier of (Image g) ; :: thesis: verum