for G, F being finite commutative Group
for a being Element of G
for f being Homomorphism of G,F holds ord (f . a) <= ord a