let k, n, p be Element of NAT ; :: thesis: for G being finite Group
for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
let G be finite Group; :: thesis: for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
let G1 be Subgroup of G; :: thesis: for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
let a be Element of G; :: thesis: ( card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} implies n divides k * p )
assume that
A1: card G = n and
A2: G = gr {a} and
A3: card G1 = p and
A4: G1 = gr {(a |^ k)} ; :: thesis: n divides k * p
set z = k * p;
consider m, l being Nat such that
A5: k * p = (n * m) + l and
A6: l < n by A1, NAT_1:17;
l = 0

proof

a |^ k in gr {(a |^ k)} by Th2;
then reconsider h = a |^ k as Element of G1 by A4, STRUCT_0:def 5;
assume A7: l <> 0 ; :: thesis: contradiction
a |^ (k * p) = (a |^ k) |^ p by GROUP_1:35
.= h |^ p by GROUP_4:1
.= 1_ G1 by A3, GR_CY_1:9
.= 1_ G by GROUP_2:44 ;
then A8: 1_ G = (a |^ (n * m)) * (a |^ l) by A5, GROUP_1:33
.= ((a |^ n) |^ m) * (a |^ l) by GROUP_1:35
.= ((1_ G) |^ m) * (a |^ l) by A1, GR_CY_1:9
.= (1_ G) * (a |^ l) by GROUP_1:31
.= a |^ l by GROUP_1:def 4 ;
( not a is being_of_order_0 & ord a = n ) by A1, A2, GR_CY_1:6, GR_CY_1:7;
hence contradiction by A6, A7, A8, GROUP_1:def 11; :: thesis: verum

end;

hence n divides k * p by A5, NAT_D:def 3; :: thesis: verum