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 A1: ( G is finite & ord z = d * l ) ; :: thesis: ord (z |^ d) = l
reconsider H = gr {z} as strict Subgroup of G ;
set m = d * l;
reconsider H = H as finite strict Subgroup of G by A1;
A2: card H = d * l by A1, GR_CY_1:27;
z in gr {z} by GR_CY_2:8;
then reconsider z1 = z as Element of H by STRUCT_0:def 5;
gr {z} = gr {z1} by GR_CY_2:9;
then ord (z1 |^ d) = l by A2, GR_CY_2:14;
hence ord (z |^ d) = l by A1, GROUP_8:3, GROUP_8:5; :: thesis: verum