let G be strict cyclic Group; :: thesis: for H being strict Subgroup of G holds H is cyclic Group
let H be strict Subgroup of G; :: thesis: H is cyclic Group

per cases ( H = (1). G or H <> (1). G ) ;

suppose H = (1). G ; :: thesis: H is cyclic Group

hence H is cyclic Group ; :: thesis: verum

end;

suppose A1: H <> (1). G ; :: thesis: H is cyclic Group

consider b being Element of G such that
A2: multMagma(# the carrier of G, the multF of G #) = gr {b} by GR_CY_1:def 7;
ex m being Nat st
( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds
m <= j ) )

proof

defpred S₁[ Nat] means ( 0 < $1 & b |^ $1 in H );
ex k being Nat st S₁[k] by A1, A2, Th24;
then A3: ex k being Nat st S₁[k] ;
ex m being Nat st
( S₁[m] & ( for j being Nat st S₁[j] holds
m <= j ) ) from NAT_1:sch 5(A3);
hence ex m being Nat st
( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds
m <= j ) ) ; :: thesis: verum

end;

then consider m being Nat such that
A4: 0 < m and
A5: b |^ m in H and
A6: for j being Nat st 0 < j & b |^ j in H holds
m <= j ;
set c = b |^ m;
reconsider c = b |^ m as Element of H by A5;
for a being Element of H ex i being Integer st a = c |^ i

proof

let a be Element of H; :: thesis: ex i being Integer st a = c |^ i
ex t being Integer st
( b |^ t in H & b |^ t = a )

proof

A7: a in G by GROUP_2:41;
A8: a in gr {b} by A2, GROUP_2:41;
a is Element of G by A7;
then consider j1 being Integer such that
A9: a = b |^ j1 by A8, GR_CY_1:5;
b |^ j1 in H by A9;
hence ex t being Integer st
( b |^ t in H & b |^ t = a ) by A9; :: thesis: verum

end;

then consider t being Integer such that
A10: b |^ t in H and
A11: b |^ t = a ;
ex r, s being Integer st
( 0 <= s & s < m & t = (m * r) + s )

proof

take t div m ; :: thesis: ex s being Integer st
( 0 <= s & s < m & t = (m * (t div m)) + s )
take t mod m ; :: thesis: ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) )
thus ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) ) by A4, NEWTON:64, NEWTON:65, NEWTON:66; :: thesis: verum

end;

then consider r, s being Integer such that
A12: 0 <= s and
A13: s < m and
A14: t = (m * r) + s ;
reconsider s = s as Element of NAT by A12, INT_1:3;
A15: b |^ t = (b |^ (m * r)) * (b |^ s) by A14, GROUP_1:33
.= ((b |^ m) |^ r) * (b |^ s) by GROUP_1:35 ;
A16: (b |^ m) |^ r in H by A5, Th22;
b |^ s in H

proof

set u = b |^ t;
set v = (b |^ m) |^ r;
A17: (((b |^ m) |^ r) ") * (b |^ t) = ((((b |^ m) |^ r) ") * ((b |^ m) |^ r)) * (b |^ s) by A15, GROUP_1:def 3
.= (1_ G) * (b |^ s) by GROUP_1:def 5
.= b |^ s by GROUP_1:def 4 ;
((b |^ m) |^ r) " in H by A16, GROUP_2:51;
hence b |^ s in H by A10, A17, GROUP_2:50; :: thesis: verum

end;

then s = 0 by A6, A13;
then b |^ s = 1_ G by GROUP_1:25;
then A18: b |^ t = (b |^ m) |^ r by A15, GROUP_1:def 4;
(b |^ m) |^ r = c |^ r by GROUP_4:2;
hence ex i being Integer st a = c |^ i by A11, A18; :: thesis: verum

end;

then H = gr {c} by GR_CY_2:5;
hence H is cyclic Group by GR_CY_2:4; :: thesis: verum

end;

end;