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