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 Def22

.= h .: (dom h) by FUNCT_2:def 1

.= rng h by RELAT_1:113 ;

hence rng h = the carrier of (Image h) ; :: thesis: verum

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 Def22

.= h .: (dom h) by FUNCT_2:def 1

.= rng h by RELAT_1:113 ;

hence rng h = the carrier of (Image h) ; :: thesis: verum