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

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