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 & s <> 0 ) by A2, A3, GR_CY_1:6;
A5: p <> 0 by A2, A3;
A6: 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
A7: (a |^ p) |^ k = 1_ G and
A8: ( k <> 0 & s > k ) ; :: thesis: contradiction
A9: a |^ (p * k) = 1_ G by A7, GROUP_1:35;
A10: ( ord a = n & not a is being_of_order_0 ) by A1, A2, GR_CY_1:6, GR_CY_1:7;
( p * s > p * k & p * k <> 0 ) by A5, A8, XCMPLX_1:6, XREAL_1:68;
hence contradiction by A3, A10, A9, GROUP_1:def 11; :: thesis: verum

end;

(a |^ p) |^ s = a |^ n by A3, GROUP_1:35
.= 1_ G by A2, GR_CY_1:9 ;
hence ord (a |^ p) = s by A4, A6, GROUP_1:def 11; :: thesis: verum