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

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