let k be Element of NAT ; :: thesis: for G being finite Group

for a being Element of G holds ord a divides k * (ord (a |^ k))

let G be finite Group; :: thesis: for a being Element of G holds ord a divides k * (ord (a |^ k))

let a be Element of G; :: thesis: 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; :: thesis: verum

for a being Element of G holds ord a divides k * (ord (a |^ k))

let G be finite Group; :: thesis: for a being Element of G holds ord a divides k * (ord (a |^ k))

let a be Element of G; :: thesis: 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; :: thesis: verum