for G1, G2 being Group
for f being Function of the carrier of G1, the carrier of G2
for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A)