let G, F be finite commutative Group; :: thesis: for a being Element of G

for f being Homomorphism of G,F st f 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 is one-to-one holds

ord (f . a) = ord a

let f be Homomorphism of G,F; :: thesis: ( f is one-to-one implies ord (f . a) = ord a )

assume AS: f is one-to-one ; :: 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;

dom f = the carrier of G by FUNCT_2:def 1;

then the carrier of (gr {a}), the carrier of (gr {(f . a)}) are_equipotent by P1, AS, CARD_1:33, GROUP_2:def 5;

hence ord (f . a) = ord a by P2, P3, CARD_1:5; :: thesis: verum

for f being Homomorphism of G,F st f 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 is one-to-one holds

ord (f . a) = ord a

let f be Homomorphism of G,F; :: thesis: ( f is one-to-one implies ord (f . a) = ord a )

assume AS: f is one-to-one ; :: 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;

dom f = the carrier of G by FUNCT_2:def 1;

then the carrier of (gr {a}), the carrier of (gr {(f . a)}) are_equipotent by P1, AS, CARD_1:33, GROUP_2:def 5;

hence ord (f . a) = ord a by P2, P3, CARD_1:5; :: thesis: verum