let G be finite Group; :: thesis:
let H be strict Subgroup of G; :: thesis:
A1: card H >= 1 by GROUP_1:45;
assume G is cyclic ; :: thesis:
then consider a being Element of G such that
A2: for b being Element of G ex n being Nat st b = a |^ n by Th18;

end;

defpred S₁[ Nat] means ( $1 > 0 & a |^ $1 is Element of H );
consider h being Element of H such that
A4: h <> 1_ H by A3, Th11;
h is Element of G by GROUP_2:42;
then consider n being Nat such that
A5: h = a |^ n by A2;
n <> 0

end;

then A6: ex n being Nat st S₁[n] by A5;
ex h1 being Element of H st
for b being Element of H ex s being Nat st b = h1 |^ s

ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A6);
then consider n being Nat such that
A7: n > 0 and
A8: a |^ n is Element of H and
A9: for k being Nat st k > 0 & a |^ k is Element of H holds
n <= k ;
consider h1 being Element of H such that
A10: h1 = a |^ n by A8;
take h1 ; :: thesis:
for b being Element of H ex s being Nat st b = h1 |^ s

let b be Element of H; :: thesis:
b is Element of G by GROUP_2:42;
then consider p being Nat such that
A11: b = a |^ p by A2;
consider s, r being Nat such that
A12: p = (n * s) + r and
A13: r < n by A7, NAT_1:17;
reconsider s = s, r = r as Element of NAT by ORDINAL1:def 12;
take s ; :: thesis:
r = 0

h1 |^ s = (a |^ n) |^ s by A10, GROUP_4:1;
then (h1 |^ s) " = ((a |^ n) |^ s) " by GROUP_2:48
.= (a |^ (n * s)) " by GROUP_1:35 ;
then reconsider g = (a |^ (n * s)) " as Element of H ;
reconsider b = a |^ p as Element of H by A11;
a |^ p = (a |^ (n * s)) * (a |^ r) by A12, GROUP_1:33;
then ((a |^ (n * s)) ") * (a |^ p) = (((a |^ (n * s)) ") * (a |^ (n * s))) * (a |^ r) by GROUP_1:def 3
.= (1_ G) * (a |^ r) by GROUP_1:def 5
.= a |^ r by GROUP_1:def 4 ;
then A14: g * b = a |^ r by GROUP_2:43;
assume r <> 0 ; :: thesis:
hence contradiction by A9, A13, A14; :: thesis:

end;

end;

hence for b being Element of H ex s being Nat st b = h1 |^ s ; :: thesis:

end;

end;