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 )

( i <> i1 & g |^ i = g |^ i1 ) )

( i <> i1 & g |^ i = g |^ i1 ) ) by A2; :: thesis: verum

( 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

( Gc is finite implies ex i, i1 being Integer st
given i, i1 being Integer such that A3:
i <> i1
and

A4: g |^ i = g |^ i1 ; :: thesis: Gc is finite

end;A4: g |^ i = g |^ i1 ; :: thesis: Gc is finite

now :: thesis: Gc is finite end;

hence
Gc is finite
; :: thesis: verumper cases
( i < i1 or i1 < i )
by A3, XXREAL_0:1;

end;

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 )

end;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

ex F being FinSequence st rng F = the carrier of Gc
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;( 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

proof

hence
Gc is finite
; :: thesis: verum
deffunc H_{1}( 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_{1}(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

A22: for y being set st y in rng F holds

ex n being Element of NAT st y = g |^ n

end;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

A11: dom F = Seg m by A9, FINSEQ_1:def 3;

A12: the carrier of Gc c= rng F

proof

take
F
; :: thesis: rng F = the carrier of Gc
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 )

end;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

hence
y in rng F
by FUNCT_1:def 3; :: thesis: verum
consider n being Element of NAT such that

A14: a = g |^ n and

n >= 0 and

A15: n < i1 - i by A8, A13;

end;A14: a = g |^ n and

n >= 0 and

A15: n < i1 - i by A8, A13;

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

end;

suppose A16:
n = 0
; :: thesis: ex n being Element of NAT st

( n in dom F & F . n = a )

( 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;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

suppose
n > 0
; :: thesis: ex n being Element of NAT st

( n in dom F & F . n = a )

( 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;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

A22: for y being set st y in rng F holds

ex n being Element of NAT st y = g |^ n

proof

rng F c= the carrier of Gc
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;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

proof

hence
rng F = the carrier of Gc
by A12, XBOOLE_0:def 10; :: thesis: verum
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;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

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 )

end;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

ex F being FinSequence st rng F = the carrier of Gc
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;( 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

proof

hence
Gc is finite
; :: thesis: verum
deffunc H_{1}( 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_{1}(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

A42: for y being set st y in rng F holds

ex n being Element of NAT st y = g |^ n

end;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

A31: dom F = Seg m by A29, FINSEQ_1:def 3;

A32: the carrier of Gc c= rng F

proof

take
F
; :: thesis: rng F = the carrier of Gc
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 )

end;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

hence
y in rng F
by FUNCT_1:def 3; :: thesis: verum
consider n being Element of NAT such that

A34: a = g |^ n and

n >= 0 and

A35: n < i - i1 by A28, A33;

end;A34: a = g |^ n and

n >= 0 and

A35: n < i - i1 by A28, A33;

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

end;

suppose A36:
n = 0
; :: thesis: ex n being Element of NAT st

( n in dom F & F . n = a )

( 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;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

suppose
n > 0
; :: thesis: ex n being Element of NAT st

( n in dom F & F . n = a )

( 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;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

A42: for y being set st y in rng F holds

ex n being Element of NAT st y = g |^ n

proof

rng F c= the carrier of Gc
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;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

proof

hence
rng F = the carrier of Gc
by A32, XBOOLE_0:def 10; :: thesis: verum
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;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

( i <> i1 & g |^ i = g |^ i1 ) )

proof

hence
( Gc is finite iff ex i, i1 being Integer st
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;( 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

( i <> i1 & g |^ i = g |^ i1 ) ) by A2; :: thesis: verum