let G, F be finite commutative Group; :: thesis: for a being Element of G
for f being Homomorphism of G,F holds ord (f . a) <= ord a
let a be Element of G; :: thesis: for f being Homomorphism of G,F holds ord (f . a) <= ord a
let f be Homomorphism of G,F; :: thesis: ord (f . a) <= ord a
P1: the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a}) by LM204L;
P2: card (gr {a}) = ord a by GR_CY_1:7;
P3: card (gr {(f . a)}) = ord (f . a) by GR_CY_1:7;
Segm (card the carrier of (gr {(f . a)})) c= Segm (card the carrier of (gr {a})) by P1, CARD_1:67;
hence ord (f . a) <= ord a by P2, P3, NAT_1:39; :: thesis: verum