let O be set ; :: thesis: for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds rng h = the carrier of (Image h)
let G, H be GroupWithOperators of O; :: thesis: for h being Homomorphism of G,H holds rng h = the carrier of (Image h)
let h be Homomorphism of G,H; :: thesis: rng h = the carrier of (Image h)
the carrier of (Image h) = h .: the carrier of G by Def25
.= h .: (dom h) by FUNCT_2:def 1
.= rng h by RELAT_1:113 ;
hence rng h = the carrier of (Image h) ; :: thesis: verum