theorem LM204L: :: GROUP_18:12
for G, F being finite commutative Group
for a being Element of G
for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})