let G, F be finite commutative Group; :: thesis: for a being Element of G
for f being Homomorphism of G,F st f | the carrier of (gr {a}) is one-to-one holds
ord (f . a) = ord a
let a be Element of G; :: thesis: for f being Homomorphism of G,F st f | the carrier of (gr {a}) is one-to-one holds
ord (f . a) = ord a
let f be Homomorphism of G,F; :: thesis: ( f | the carrier of (gr {a}) is one-to-one implies ord (f . a) = ord a )
assume AS: f | the carrier of (gr {a}) is one-to-one ; :: thesis: ord (f . a) = ord a
reconsider H = f | the carrier of (gr {a}) as Homomorphism of (gr {a}),F by LM204G;
a in gr {a} by GR_CY_2:2;
then reconsider a0 = a as Element of (gr {a}) ;
f . a = H . a0 by FUNCT_1:49;
hence ord (f . a) = ord a0 by AS, LM204F
.= card (gr {a0}) by GR_CY_1:7
.= card (gr {a}) by GR_CY_2:3
.= ord a by GR_CY_1:7 ;
:: thesis: verum