let G be finite Group; :: thesis: for H being strict Subgroup of G st G is cyclic holds
H is cyclic
let H be strict Subgroup of G; :: thesis: ( G is cyclic implies H is cyclic )
assume A1: G is cyclic ; :: thesis: H is cyclic
consider a being Element of G such that
A2: for b being Element of G ex n being Element of NAT st b = a |^ n by A1, Th42;
A3: card H >= 1 by GROUP_1:90;

per cases ( card H = 1 or card H > 1 ) by A3, XXREAL_0:1;

suppose card H = 1 ; :: thesis: H is cyclic

then H = (1). G by GROUP_2:82;
hence H is cyclic ; :: thesis: verum

end;

suppose card H > 1 ; :: thesis: H is cyclic

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

proof

assume n = 0 ; :: thesis: contradiction
then h = 1_ G by A5, GROUP_1:43
.= 1_ H by GROUP_2:53 ;
hence contradiction by A4; :: thesis: verum

end;

then n > 0 ;
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 Element of NAT st b = h1 |^ s

proof

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 & a |^ n is Element of H ) and
A8: for k being Nat st k > 0 & a |^ k is Element of H holds
n <= k ;
consider h1 being Element of H such that
A9: h1 = a |^ n by A7;
take h1 ; :: thesis: for b being Element of H ex s being Element of NAT st b = h1 |^ s
for b being Element of H ex s being Element of NAT st b = h1 |^ s

proof

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

proof

assume r <> 0 ; :: thesis: contradiction
then A14: r > 0 ;
A15: a |^ p = (a |^ (n * s)) * (a |^ r) by A11, GROUP_1:63;
h1 |^ s = (a |^ n) |^ s by A9, GROUP_4:3;
then (h1 |^ s) " = ((a |^ n) |^ s) " by GROUP_2:57
.= (a |^ (n * s)) " by GROUP_1:67 ;
then reconsider g = (a |^ (n * s)) " as Element of H ;
reconsider b = a |^ p as Element of H by A10;
((a |^ (n * s)) " ) * (a |^ p) = (((a |^ (n * s)) " ) * (a |^ (n * s))) * (a |^ r) by A15, GROUP_1:def 4
.= (1_ G) * (a |^ r) by GROUP_1:def 6
.= a |^ r by GROUP_1:def 5 ;
then g * b = a |^ r by GROUP_2:52;
hence contradiction by A8, A12, A14; :: thesis: verum

end;

take s ; :: thesis: b = h1 |^ s
a |^ p = (a |^ n) |^ s by A11, A13, GROUP_1:67
.= h1 |^ s by A9, GROUP_4:3 ;
hence b = h1 |^ s by A10; :: thesis: verum

end;

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

end;

hence H is cyclic by Th42; :: thesis: verum

end;

end;