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 9;
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 Element of 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 & b |^ m in H & ( 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 A4, STRUCT_0:def 5;
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

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

end;

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

proof

take r = t div m; :: thesis: ex s being Integer st
( 0 <= s & s < m & t = (m * r) + s )
take s = t mod m; :: thesis: ( 0 <= s & s < m & t = (m * r) + s )
thus ( 0 <= s & s < m & t = (m * r) + s ) by A4, NEWTON:78, NEWTON:79, NEWTON:80; :: thesis: verum

end;

then consider r, s being Integer such that
A9: ( 0 <= s & s < m & t = (m * r) + s ) ;
reconsider s = s as Element of NAT by A9, INT_1:16;
A10: b |^ t = (b |^ (m * r)) * (b |^ s) by A9, GROUP_1:63
.= ((b |^ m) |^ r) * (b |^ s) by GROUP_1:67 ;
A11: (b |^ m) |^ r in H by A4, Th22;
A12: b |^ s in H

proof

set u = b |^ t;
set v = (b |^ m) |^ r;
A13: (((b |^ m) |^ r) " ) * (b |^ t) = ((((b |^ m) |^ r) " ) * ((b |^ m) |^ r)) * (b |^ s) by A10, GROUP_1:def 4
.= (1_ G) * (b |^ s) by GROUP_1:def 6
.= b |^ s by GROUP_1:def 5 ;
((b |^ m) |^ r) " in H by A11, GROUP_2:60;
hence b |^ s in H by A8, A13, GROUP_2:59; :: thesis: verum

end;

b |^ s = 1_ G

proof

s = 0 by A4, A9, A12;
hence b |^ s = 1_ G by GROUP_1:43; :: thesis: verum

end;

then A14: b |^ t = (b |^ m) |^ r by A10, GROUP_1:def 5;
(b |^ m) |^ r = c |^ r by GROUP_4:4;
hence ex i being Integer st a = c |^ i by A8, A14; :: thesis: verum

end;

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

end;

end;