let k be Element of NAT ; for G being finite Group
for a being Element of G holds ord a divides k * (ord (a |^ k))
let G be finite Group; for a being Element of G holds ord a divides k * (ord (a |^ k))
let a be Element of G; ord a divides k * (ord (a |^ k))
a in gr {a}
by GR_CY_2:2;
then reconsider a0 = a as Element of (gr {a}) ;
A11:
gr {a0} = gr {a}
by GR_CY_2:3;
A12:
card (gr {a}) = ord a
by GR_CY_1:7;
( ord (a |^ k) = card (gr {(a |^ k)}) & card (gr {(a |^ k)}) = card (gr {(a0 |^ k)}) )
by GR_CY_1:7, GROUP_4:2, GR_CY_2:3;
hence
ord a divides k * (ord (a |^ k))
by A11, A12, GR_CY_2:11; verum