let G be Group; :: thesis: for z being Element of G
for d, l being Element of NAT st G is finite & ord z = d * l holds
ord (z |^ d) = l
let z be Element of G; :: thesis: for d, l being Element of NAT st G is finite & ord z = d * l holds
ord (z |^ d) = l
let d, l be Element of NAT ; :: thesis: ( G is finite & ord z = d * l implies ord (z |^ d) = l )
assume that
A1: G is finite and
A2: ord z = d * l ; :: thesis: ord (z |^ d) = l
set m = d * l;
reconsider H = gr {z} as strict Subgroup of G ;
reconsider H = H as finite strict Subgroup of G by A1;
z in gr {z} by GR_CY_2:2;
then reconsider z1 = z as Element of H ;
A3: gr {z} = gr {z1} by GR_CY_2:3;
card H = d * l by A1, A2, GR_CY_1:7;
then ord (z1 |^ d) = l by A3, GR_CY_2:8;
hence ord (z |^ d) = l by A1, GROUP_8:3, GROUP_8:5; :: thesis: verum