let Gc be cyclic Group; :: thesis: for g being Element of Gc st Gc = gr {g} holds
( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )
let g be Element of Gc; :: thesis: ( Gc = gr {g} implies ( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) ) )
assume A1: Gc = gr {g} ; :: thesis: ( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )
A2: ( ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) implies Gc is finite )

proof

given i, i1 being Integer such that A3: i <> i1 and
A4: g |^ i = g |^ i1 ; :: thesis: Gc is finite

now :: thesis: Gc is finite

per cases ( i < i1 or i1 < i ) by A3, XXREAL_0:1;

suppose A5: i < i1 ; :: thesis: Gc is finite

set r = i1 - i;
i1 > i + 0 by A5;
then A6: i1 - i > 0 by XREAL_1:20;
then reconsider m = i1 - i as Element of NAT by INT_1:3;
(g |^ i1) * (g |^ (- i)) = (g |^ i) * ((g |^ i) ") by A4, GROUP_1:36;
then (g |^ i1) * (g |^ (- i)) = 1_ Gc by GROUP_1:def 5;
then A7: g |^ (i1 + (- i)) = 1_ Gc by GROUP_1:33;
A8: for i2 being Integer ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i1 - i )

proof

let i2 be Integer; :: thesis: ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i1 - i )
reconsider m = i2 mod (i1 - i) as Element of NAT by A6, INT_1:3, NEWTON:64;
take m ; :: thesis: ( g |^ i2 = g |^ m & m >= 0 & m < i1 - i )
g |^ i2 = g |^ (((i2 div (i1 - i)) * (i1 - i)) + (i2 mod (i1 - i))) by A6, NEWTON:66
.= (g |^ ((i1 - i) * (i2 div (i1 - i)))) * (g |^ (i2 mod (i1 - i))) by GROUP_1:33
.= ((1_ Gc) |^ (i2 div (i1 - i))) * (g |^ (i2 mod (i1 - i))) by A7, GROUP_1:35
.= (1_ Gc) * (g |^ (i2 mod (i1 - i))) by GROUP_1:31
.= g |^ (i2 mod (i1 - i)) by GROUP_1:def 4 ;
hence ( g |^ i2 = g |^ m & m >= 0 & m < i1 - i ) by A6, NEWTON:65; :: thesis: verum

end;

ex F being FinSequence st rng F = the carrier of Gc

proof

deffunc H₁( Nat) -> Element of the carrier of Gc = g |^ $1;
consider F being FinSequence such that
A9: len F = m and
A10: for p being Nat st p in dom F holds
F . p = H₁(p) from FINSEQ_1:sch 2();
A11: dom F = Seg m by A9, FINSEQ_1:def 3;
A12: the carrier of Gc c= rng F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of Gc or y in rng F )
assume y in the carrier of Gc ; :: thesis: y in rng F
then reconsider a = y as Element of Gc ;
a in Gc by STRUCT_0:def 5;
then A13: ex i2 being Integer st a = g |^ i2 by A1, GR_CY_1:5;
ex n being Element of NAT st
( n in dom F & F . n = a )

proof

consider n being Element of NAT such that
A14: a = g |^ n and
n >= 0 and
A15: n < i1 - i by A8, A13;

per cases ( n = 0 or n > 0 ) ;

suppose A16: n = 0 ; :: thesis: ex n being Element of NAT st
( n in dom F & F . n = a )

A17: m >= 0 + 1 by A6, NAT_1:13;
then A18: m in Seg m by FINSEQ_1:1;
A19: m in dom F by A11, A17, FINSEQ_1:1;
a = g |^ m by A7, A14, A16, GROUP_1:25;
then F . m = a by A10, A11, A18;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A19; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex n being Element of NAT st
( n in dom F & F . n = a )

then A20: n >= 0 + 1 by NAT_1:13;
then n in Seg m by A15, FINSEQ_1:1;
then A21: F . n = a by A10, A11, A14;
n in dom F by A11, A15, A20, FINSEQ_1:1;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A21; :: thesis: verum

end;

end;

end;

hence y in rng F by FUNCT_1:def 3; :: thesis: verum

end;

take F ; :: thesis: rng F = the carrier of Gc
A22: for y being set st y in rng F holds
ex n being Element of NAT st y = g |^ n

proof

let y be set ; :: thesis: ( y in rng F implies ex n being Element of NAT st y = g |^ n )
assume y in rng F ; :: thesis: ex n being Element of NAT st y = g |^ n
then consider x being object such that
A23: x in dom F and
A24: F . x = y by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A23;
take n ; :: thesis: y = g |^ n
thus y = g |^ n by A10, A23, A24; :: thesis: verum

end;

rng F c= the carrier of Gc

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of Gc )
assume y in rng F ; :: thesis: y in the carrier of Gc
then ex n being Element of NAT st y = g |^ n by A22;
hence y in the carrier of Gc ; :: thesis: verum

end;

hence rng F = the carrier of Gc by A12, XBOOLE_0:def 10; :: thesis: verum

end;

hence Gc is finite ; :: thesis: verum

end;

suppose A25: i1 < i ; :: thesis: Gc is finite

set r = i - i1;
i > i1 + 0 by A25;
then A26: i - i1 > 0 by XREAL_1:20;
then reconsider m = i - i1 as Element of NAT by INT_1:3;
(g |^ i) * (g |^ (- i1)) = (g |^ i1) * ((g |^ i1) ") by A4, GROUP_1:36;
then (g |^ i) * (g |^ (- i1)) = 1_ Gc by GROUP_1:def 5;
then A27: g |^ (i + (- i1)) = 1_ Gc by GROUP_1:33;
A28: for i2 being Integer ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i - i1 )

proof

let i2 be Integer; :: thesis: ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i - i1 )
reconsider m = i2 mod (i - i1) as Element of NAT by A26, INT_1:3, NEWTON:64;
take m ; :: thesis: ( g |^ i2 = g |^ m & m >= 0 & m < i - i1 )
g |^ i2 = g |^ (((i2 div (i - i1)) * (i - i1)) + (i2 mod (i - i1))) by A26, NEWTON:66
.= (g |^ ((i - i1) * (i2 div (i - i1)))) * (g |^ (i2 mod (i - i1))) by GROUP_1:33
.= ((1_ Gc) |^ (i2 div (i - i1))) * (g |^ (i2 mod (i - i1))) by A27, GROUP_1:35
.= (1_ Gc) * (g |^ (i2 mod (i - i1))) by GROUP_1:31
.= g |^ (i2 mod (i - i1)) by GROUP_1:def 4 ;
hence ( g |^ i2 = g |^ m & m >= 0 & m < i - i1 ) by A26, NEWTON:65; :: thesis: verum

end;

ex F being FinSequence st rng F = the carrier of Gc

proof

deffunc H₁( Nat) -> Element of the carrier of Gc = g |^ $1;
consider F being FinSequence such that
A29: len F = m and
A30: for p being Nat st p in dom F holds
F . p = H₁(p) from FINSEQ_1:sch 2();
A31: dom F = Seg m by A29, FINSEQ_1:def 3;
A32: the carrier of Gc c= rng F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of Gc or y in rng F )
assume y in the carrier of Gc ; :: thesis: y in rng F
then reconsider a = y as Element of Gc ;
a in Gc by STRUCT_0:def 5;
then A33: ex i2 being Integer st a = g |^ i2 by A1, GR_CY_1:5;
ex n being Element of NAT st
( n in dom F & F . n = a )

proof

consider n being Element of NAT such that
A34: a = g |^ n and
n >= 0 and
A35: n < i - i1 by A28, A33;

per cases ( n = 0 or n > 0 ) ;

suppose A36: n = 0 ; :: thesis: ex n being Element of NAT st
( n in dom F & F . n = a )

A37: m >= 0 + 1 by A26, NAT_1:13;
then A38: m in Seg m by FINSEQ_1:1;
A39: m in dom F by A31, A37, FINSEQ_1:1;
a = g |^ m by A27, A34, A36, GROUP_1:25;
then F . m = a by A30, A31, A38;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A39; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex n being Element of NAT st
( n in dom F & F . n = a )

then A40: n >= 0 + 1 by NAT_1:13;
then n in Seg m by A35, FINSEQ_1:1;
then A41: F . n = a by A30, A31, A34;
n in dom F by A31, A35, A40, FINSEQ_1:1;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A41; :: thesis: verum

end;

end;

end;

hence y in rng F by FUNCT_1:def 3; :: thesis: verum

end;

take F ; :: thesis: rng F = the carrier of Gc
A42: for y being set st y in rng F holds
ex n being Element of NAT st y = g |^ n

proof

let y be set ; :: thesis: ( y in rng F implies ex n being Element of NAT st y = g |^ n )
assume y in rng F ; :: thesis: ex n being Element of NAT st y = g |^ n
then consider x being object such that
A43: x in dom F and
A44: F . x = y by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A43;
take n ; :: thesis: y = g |^ n
thus y = g |^ n by A30, A43, A44; :: thesis: verum

end;

rng F c= the carrier of Gc

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of Gc )
assume y in rng F ; :: thesis: y in the carrier of Gc
then ex n being Element of NAT st y = g |^ n by A42;
hence y in the carrier of Gc ; :: thesis: verum

end;

hence rng F = the carrier of Gc by A32, XBOOLE_0:def 10; :: thesis: verum

end;

hence Gc is finite ; :: thesis: verum

end;

end;

end;

hence Gc is finite ; :: thesis: verum

end;

( Gc is finite implies ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )

proof

assume Gc is finite ; :: thesis: ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 )
then reconsider Gc = Gc as finite cyclic Group ;
reconsider z = 0 , i0 = card Gc as Integer ;
A45: g |^ z = 1_ Gc by GROUP_1:25
.= g |^ i0 by GR_CY_1:9 ;
thus ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) by A45; :: thesis: verum

end;

hence ( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) ) by A2; :: thesis: verum