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

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