let G, H be Group; :: thesis: for g being Homomorphism of G,H
for A being Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A
let g be Homomorphism of G,H; :: thesis: for A being Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A
let A be Subgroup of G; :: thesis: the carrier of (g .: A) = g .: the carrier of A
thus the carrier of (g .: A) = rng (g | A) by GROUP_6:44
.= g .: the carrier of A by RELAT_1:115 ; :: thesis: verum