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 )
A1: card H >= 1 by GROUP_1:45;
assume G is cyclic ; :: thesis: H is cyclic
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;

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

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

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

end;

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

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

proof

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

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

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 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
for b being Element of H ex s being Nat st b = h1 |^ s

proof

let b be Element of H; :: thesis: ex s being Nat st b = h1 |^ s
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: b = h1 |^ s
r = 0

proof

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: contradiction
hence contradiction by A9, A13, A14; :: thesis: verum

end;

then a |^ p = (a |^ n) |^ s by A12, GROUP_1:35
.= h1 |^ s by A10, GROUP_4:1 ;
hence b = h1 |^ s by A11; :: thesis: verum

end;

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

end;

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

end;

end;