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 ;
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 ;
A10: ( ord a = n & not a is being_of_order_0 ) by ;
( p * s > p * k & p * k <> 0 ) by ;
hence contradiction by A3, A10, A9, GROUP_1:def 11; :: thesis: verum
end;
(a |^ p) |^ s = a |^ n by
.= 1_ G by ;
hence ord (a |^ p) = s by ; :: thesis: verum