let G be finite Group; :: thesis: for a being Element of G
for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds
ord (a |^ p) = s
let a be Element of G; :: thesis: for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds
ord (a |^ p) = s
let n, p, s be Element of NAT ; :: thesis: ( card (gr {a}) = n & n = p * s implies ord (a |^ p) = s )
assume AS1: ( card (gr {a}) = n & n = p * s ) ; :: thesis: ord (a |^ p) = s
reconsider a0 = a as Element of (gr {a}) by GR_CY_2:2, STRUCT_0:def 5;
A0: gr {a0} = gr {a} by GR_CY_2:3;
ord (a0 |^ p) = card (gr {(a0 |^ p)}) by GR_CY_1:7
.= card (gr {(a |^ p)}) by GROUP_4:2, GR_CY_2:3
.= ord (a |^ p) by GR_CY_1:7 ;
hence ord (a |^ p) = s by A0, AS1, GR_CY_2:8; :: thesis: verum