let n, p, s be Element of NAT ; :: thesis: for G being finite Group
for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
let G be finite Group; :: thesis: for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
let a be Element of G; :: thesis: ( G = gr {a} & card G = n & n = p * s implies ord (a |^ p) = s )
assume that
A1: G = gr {a} and
A2: card G = n and
A3: n = p * s ; :: thesis: ord (a |^ p) = s
A4: not a |^ p is being_of_order_0 by GR_CY_1:26;
A5: (a |^ p) |^ s = 1_ G

proof

thus (a |^ p) |^ s = a |^ n by A3, GROUP_1:67
.= 1_ G by A2, GR_CY_1:29 ; :: thesis: verum

end;

A6: s <> 0 by A2, A3, GROUP_1:90;
A7: p <> 0 by A2, A3, GROUP_1:90;
for k being Nat st (a |^ p) |^ k = 1_ G & k <> 0 holds
s <= k

proof

let k be Nat; :: thesis: ( (a |^ p) |^ k = 1_ G & k <> 0 implies s <= k )
assume that
A8: (a |^ p) |^ k = 1_ G and
A9: k <> 0 and
A10: s > k ; :: thesis: contradiction
A11: p * s > p * k by A7, A10, XREAL_1:70;
A12: ord a = n by A1, A2, GR_CY_1:27;
A13: p * k <> 0 by A7, A9, XCMPLX_1:6;
A14: not a is being_of_order_0 by GR_CY_1:26;
a |^ (p * k) = 1_ G by A8, GROUP_1:67;
hence contradiction by A3, A11, A12, A13, A14, GROUP_1:def 12; :: thesis: verum

end;

hence ord (a |^ p) = s by A4, A5, A6, GROUP_1:def 12; :: thesis: verum