let n, p, k 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;
n > 0 by A1, GROUP_1:90;
then consider m, l being Nat such that
A5: k * p = (n * m) + l and
A6: l < n by NAT_1:17;
l = 0

proof

assume A7: l <> 0 ; :: thesis: contradiction
a |^ k in gr {(a |^ k)} by Th8;
then reconsider h = a |^ k as Element of G1 by A4, STRUCT_0:def 5;
a |^ (k * p) = (a |^ k) |^ p by GROUP_1:67
.= h |^ p by GROUP_4:3
.= 1_ G1 by A3, GR_CY_1:29
.= 1_ G by GROUP_2:53 ;
then A8: 1_ G = (a |^ (n * m)) * (a |^ l) by A5, GROUP_1:63
.= ((a |^ n) |^ m) * (a |^ l) by GROUP_1:67
.= ((1_ G) |^ m) * (a |^ l) by A1, GR_CY_1:29
.= (1_ G) * (a |^ l) by GROUP_1:61
.= a |^ l by GROUP_1:def 5 ;
A9: not a is being_of_order_0 by GR_CY_1:26;
ord a = n by A1, A2, GR_CY_1:27;
hence contradiction by A6, A7, A8, A9, GROUP_1:def 12; :: thesis: verum

end;

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