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: ( 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 zero = 0 , i0 = card Gc as Integer ;
A3: zero <> i0 by GROUP_1:90;
g |^ zero = 1_ Gc by GROUP_1:43
.= g |^ i0 by GR_CY_1:29 ;
hence ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) by A3; :: thesis: verum

end;

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

proof

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

now

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

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

then i1 > i + 0 ;
then A5: i1 - i > 0 by XREAL_1:22;
set r = i1 - i;
A6: g |^ (i1 - i) = 1_ Gc

proof

(g |^ i1) * (g |^ (- i)) = (g |^ i) * ((g |^ i) " ) by A4, GROUP_1:70;
then (g |^ i1) * (g |^ (- i)) = 1_ Gc by GROUP_1:def 6;
then g |^ (i1 + (- i)) = 1_ Gc by GROUP_1:63;
hence g |^ (i1 - i) = 1_ Gc ; :: thesis: verum

end;

A7: 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 )
A8: g |^ i2 = g |^ (((i2 div (i1 - i)) * (i1 - i)) + (i2 mod (i1 - i))) by A5, NEWTON:80
.= (g |^ ((i1 - i) * (i2 div (i1 - i)))) * (g |^ (i2 mod (i1 - i))) by GROUP_1:63
.= ((1_ Gc) |^ (i2 div (i1 - i))) * (g |^ (i2 mod (i1 - i))) by A6, GROUP_1:67
.= (1_ Gc) * (g |^ (i2 mod (i1 - i))) by GROUP_1:61
.= g |^ (i2 mod (i1 - i)) by GROUP_1:def 5 ;
reconsider m = i2 mod (i1 - i) as Element of NAT by A5, INT_1:16, NEWTON:78;
take m ; :: thesis: ( g |^ i2 = g |^ m & m >= 0 & m < i1 - i )
thus ( g |^ i2 = g |^ m & m >= 0 & m < i1 - i ) by A5, A8, NEWTON:79; :: thesis: verum

end;

reconsider m = i1 - i as Element of NAT by A5, INT_1:16;
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: 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 set such that
A13: x in dom F and
A14: F . x = y by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A13;
take n ; :: thesis: y = g |^ n
thus y = g |^ n by A10, A13, A14; :: thesis: verum

end;

A15: rng F c= the carrier of Gc

proof

let y be set ; :: 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 consider n being Element of NAT such that
A16: y = g |^ n by A12;
thus y in the carrier of Gc by A16; :: thesis: verum

end;

A17: the carrier of Gc c= rng F

proof

let y be set ; :: 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 A18: ex i2 being Integer st a = g |^ i2 by A1, GR_CY_1:25;
ex n being Element of NAT st
( n in dom F & F . n = a )

proof

consider n being Element of NAT such that
A19: a = g |^ n and
n >= 0 and
A20: n < i1 - i by A7, A18;

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

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

then A21: a = g |^ m by A6, A19, GROUP_1:43;
A22: m >= 1

proof

m >= 0 + 1 by A5, NAT_1:13;
hence m >= 1 ; :: thesis: verum

end;

then A23: m in Seg m by FINSEQ_1:3;
A24: m in dom F by A11, A22, FINSEQ_1:3;
F . m = a by A10, A21, A23, A11;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A24; :: thesis: verum

end;

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

A26: n >= 1

proof

n >= 0 + 1 by A25, NAT_1:13;
hence n >= 1 ; :: thesis: verum

end;

then A27: n in Seg m by A20, FINSEQ_1:3;
A28: n in dom F by A11, A20, A26, FINSEQ_1:3;
F . n = a by A10, A19, A27, A11;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A28; :: thesis: verum

end;

end;

end;

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

end;

take F ; :: thesis: rng F = the carrier of Gc
thus rng F = the carrier of Gc by A15, A17, XBOOLE_0:def 10; :: thesis: verum

end;

hence Gc is finite ; :: thesis: verum

end;

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

then i > i1 + 0 ;
then A29: i - i1 > 0 by XREAL_1:22;
set r = i - i1;
A30: g |^ (i - i1) = 1_ Gc

proof

(g |^ i) * (g |^ (- i1)) = (g |^ i1) * ((g |^ i1) " ) by A4, GROUP_1:70;
then (g |^ i) * (g |^ (- i1)) = 1_ Gc by GROUP_1:def 6;
then g |^ (i + (- i1)) = 1_ Gc by GROUP_1:63;
hence g |^ (i - i1) = 1_ Gc ; :: thesis: verum

end;

A31: 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 )
A32: g |^ i2 = g |^ (((i2 div (i - i1)) * (i - i1)) + (i2 mod (i - i1))) by A29, NEWTON:80
.= (g |^ ((i - i1) * (i2 div (i - i1)))) * (g |^ (i2 mod (i - i1))) by GROUP_1:63
.= ((1_ Gc) |^ (i2 div (i - i1))) * (g |^ (i2 mod (i - i1))) by A30, GROUP_1:67
.= (1_ Gc) * (g |^ (i2 mod (i - i1))) by GROUP_1:61
.= g |^ (i2 mod (i - i1)) by GROUP_1:def 5 ;
reconsider m = i2 mod (i - i1) as Element of NAT by A29, INT_1:16, NEWTON:78;
take m ; :: thesis: ( g |^ i2 = g |^ m & m >= 0 & m < i - i1 )
thus ( g |^ i2 = g |^ m & m >= 0 & m < i - i1 ) by A29, A32, NEWTON:79; :: thesis: verum

end;

reconsider m = i - i1 as Element of NAT by A29, INT_1:16;
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
A33: len F = m and
A34: for p being Nat st p in dom F holds
F . p = H₁(p) from FINSEQ_1:sch 2();
A35: dom F = Seg m by A33, FINSEQ_1:def 3;
A36: 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 set such that
A37: x in dom F and
A38: F . x = y by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A37;
take n ; :: thesis: y = g |^ n
thus y = g |^ n by A34, A37, A38; :: thesis: verum

end;

A39: rng F c= the carrier of Gc

proof

let y be set ; :: 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 consider n being Element of NAT such that
A40: y = g |^ n by A36;
thus y in the carrier of Gc by A40; :: thesis: verum

end;

A41: the carrier of Gc c= rng F

proof

let y be set ; :: 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 A42: ex i2 being Integer st a = g |^ i2 by A1, GR_CY_1:25;
ex n being Element of NAT st
( n in dom F & F . n = a )

proof

consider n being Element of NAT such that
A43: a = g |^ n and
n >= 0 and
A44: n < i - i1 by A31, A42;

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

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

then A45: a = g |^ m by A30, A43, GROUP_1:43;
A46: m >= 1

proof

m >= 0 + 1 by A29, NAT_1:13;
hence m >= 1 ; :: thesis: verum

end;

then A47: m in Seg m by FINSEQ_1:3;
A48: m in dom F by A35, A46, FINSEQ_1:3;
F . m = a by A34, A45, A47, A35;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A48; :: thesis: verum

end;

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

A50: n >= 1

proof

n >= 0 + 1 by A49, NAT_1:13;
hence n >= 1 ; :: thesis: verum

end;

then A51: n in Seg m by A44, FINSEQ_1:3;
A52: n in dom F by A35, A44, A50, FINSEQ_1:3;
F . n = a by A34, A43, A51, A35;
hence ex n being Element of NAT st
( n in dom F & F . n = a ) by A52; :: thesis: verum

end;

end;

end;

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

end;

take F ; :: thesis: rng F = the carrier of Gc
thus rng F = the carrier of Gc by A39, A41, XBOOLE_0:def 10; :: thesis: verum

end;

hence Gc is finite ; :: thesis: verum

end;

end;

end;

hence Gc is finite ; :: thesis: verum

end;

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