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 ;
l = 0
proof
a |^ k in gr {(a |^ k)} by Th2;
then reconsider h = a |^ k as Element of G1 by ;
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
.= 1_ G by GROUP_2:44 ;
then A8: 1_ G = (a |^ (n * m)) * (a |^ l) by
.= ((a |^ n) |^ m) * (a |^ l) by GROUP_1:35
.= ((1_ G) |^ m) * (a |^ l) by
.= (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 ;
hence contradiction by A6, A7, A8, GROUP_1:def 11; :: thesis: verum
end;
hence n divides k * p by ; :: thesis: verum