:: GR_CY_1 semantic presentation

begin


registration
let n be non zero Nat;
cluster Segm n ->  non empty ;
coherence
 not Segm n is empty ;
end;

Lm1:  for x being set
for n being Nat st x in Segm n holds
x is Element of NAT
;

definition
redefine func addint  means :: GR_CY_1:def 1
 for i1, i2 being Element of INT holds it . (i1,i2) = addreal . (i1,i2);
compatibility
 for b1 being Element of bool [:[:INT,INT:],INT:] holds
( b1 = addint iff for i1, i2 being Element of INT holds b1 . (i1,i2) = addreal . (i1,i2) )
proof
let b be BinOp of INT; ::_thesis: ( b = addint iff for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2) )
hereby  ::_thesis: ( ( for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2) ) implies b = addint )
assume A1: b = addint ; ::_thesis: for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2)
let i1, i2 be Element of INT ; ::_thesis: b . (i1,i2) = addreal . (i1,i2)
thus b . (i1,i2) = i1 + i2 by A1, BINOP_2:def_20
.= addreal . (i1,i2) by BINOP_2:def_9 ; ::_thesis: verum
end;
assume A2: for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2) ; ::_thesis: b = addint
now__::_thesis:_for_i1,_i2_being_Element_of_INT_holds_b_._(i1,i2)_=_addint_._(i1,i2)
let i1, i2 be Element of INT ; ::_thesis: b . (i1,i2) = addint . (i1,i2)
thus b . (i1,i2) = addreal . (i1,i2) by A2
.= i1 + i2 by BINOP_2:def_9
.= addint . (i1,i2) by BINOP_2:def_20 ; ::_thesis: verum
end;
hence  b = addint by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines addint GR_CY_1:def_1_:_
 for b1 being Element of bool [:[:INT,INT:],INT:] holds
( b1 = addint iff for i1, i2 being Element of INT holds b1 . (i1,i2) = addreal . (i1,i2) );

theorem :: GR_CY_1:1
for i1 being Element of INT st i1 = 0 holds
i1 is_a_unity_wrt addint by BINOP_2:4, SETWISEO:14;

theorem Th2: :: GR_CY_1:2
for I being FinSequence of INT holds Sum I = addint $$ I
proof
let I be FinSequence of INT ; ::_thesis: Sum I = addint $$ I
set g = addint ;
set h = addcomplex ;
set i = [#] (I,(the_unity_wrt addint));
 rng I c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider f = I as FinSequence of COMPLEX by FINSEQ_1:def_4;
set j = [#] (f,(the_unity_wrt addcomplex));
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def_2;
A2: ( addint $$ I = addint $$ ((finSeg n),([#] (I,(the_unity_wrt addint)))) & addcomplex $$ f = addcomplex $$ ((finSeg n),([#] (f,(the_unity_wrt addcomplex)))) ) by A1, SETWOP_2:def_2;
defpred S1[ Nat] means addint $$ ((finSeg $1),([#] (I,(the_unity_wrt addint)))) = addcomplex $$ ((finSeg $1),([#] (f,(the_unity_wrt addcomplex))));
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
set b = addint $$ ((finSeg k),([#] (I,(the_unity_wrt addint))));
set a = ([#] (I,(the_unity_wrt addint))) . (k + 1);
A5: not k + 1 in Seg k by FINSEQ_3:8;
addint $$ ((finSeg (k + 1)),([#] (I,(the_unity_wrt addint)))) = addint $$ (((finSeg k) \/ {.(k + 1).}),([#] (I,(the_unity_wrt addint)))) by FINSEQ_1:9
.= addint . ((addint $$ ((finSeg k),([#] (I,(the_unity_wrt addint))))),(([#] (I,(the_unity_wrt addint))) . (k + 1))) by A5, SETWOP_2:2
.= (addint $$ ((finSeg k),([#] (I,(the_unity_wrt addint))))) + (([#] (I,(the_unity_wrt addint))) . (k + 1)) by BINOP_2:def_20
.= addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by A4, BINOP_2:1, BINOP_2:4, BINOP_2:def_3
.= addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) by A5, SETWOP_2:2
.= addcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt addcomplex)))) by FINSEQ_1:9 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A6: Seg 0 = {}. NAT ;
then addint $$ ((finSeg 0),([#] (I,(the_unity_wrt addint)))) = the_unity_wrt addcomplex by BINOP_2:1, BINOP_2:4, SETWISEO:31
.= addcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt addcomplex)))) by A6, SETWISEO:31 ;
then A7: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A7, A3);
then  addint $$ I = addcomplex $$ f by A2;
hence  Sum I = addint $$ I by RVSUM_1:def_10; ::_thesis: verum
end;

definition
let I be FinSequence of INT ;
:: original: Sum
redefine func Sum I ->  Element of INT  equals :: GR_CY_1:def 2
addint $$ I;
coherence
 Sum I is Element of INT
proof
 Sum I = addint $$ I by Th2;
hence  Sum I is Element of INT ; ::_thesis: verum
end;
compatibility
 for b1 being Element of INT holds
( b1 = Sum I iff b1 = addint $$ I ) by Th2;
end;

:: deftheorem  defines Sum GR_CY_1:def_2_:_
 for I being FinSequence of INT holds Sum I = addint $$ I;

theorem Th3: :: GR_CY_1:3
Sum (<*> INT) = 0 by BINOP_2:4, FINSOP_1:10;

Lm2:  for G being Group
for a being Element of G holds Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT))
proof
let G be Group; ::_thesis: for a being Element of G holds Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT))
let a be Element of G; ::_thesis: Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT))
 (<*> the carrier of G) |^ (<*> INT) = <*> the carrier of G by GROUP_4:21;
then  Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = 1_ G by GROUP_4:8
.= a |^ (Sum (<*> INT)) by Th3, GROUP_1:25 ;
hence  Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT)) ; ::_thesis: verum
end;

Lm3:  for G being Group
for a being Element of G
for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
proof
let G be Group; ::_thesis: for a being Element of G
for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
let a be Element of G; ::_thesis: for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
let I be FinSequence of INT ; ::_thesis: for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
let w be Element of INT ; ::_thesis: ( Product (((len I) |-> a) |^ I) = a |^ (Sum I) implies Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>)) )
assume A1: Product (((len I) |-> a) |^ I) = a |^ (Sum I) ; ::_thesis: Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
A2: len ((len I) |-> a) = len I by CARD_1:def_7;
A3: len <*a*> = 1 by FINSEQ_1:40
.= len <*w*> by FINSEQ_1:40 ;
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = Product ((((len I) + 1) |-> a) |^ (I ^ <*w*>)) by FINSEQ_2:16
.= Product ((((len I) |-> a) ^ <*a*>) |^ (I ^ <*w*>)) by FINSEQ_2:60
.= Product ((((len I) |-> a) |^ I) ^ (<*a*> |^ <*w*>)) by A2, A3, GROUP_4:19
.= (Product (((len I) |-> a) |^ I)) * (Product (<*a*> |^ <*(@ (@ w))*>)) by GROUP_4:5
.= (Product (((len I) |-> a) |^ I)) * (Product <*(a |^ (@ w))*>) by GROUP_4:22
.= (a |^ (Sum I)) * (a |^ (@ w)) by A1, FINSOP_1:11
.= a |^ ((Sum I) + (@ w)) by GROUP_1:33
.= a |^ (Sum (I ^ <*w*>)) by RVSUM_1:74 ;
hence  Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>)) ; ::_thesis: verum
end;

theorem Th4: :: GR_CY_1:4
for G being Group
for a being Element of G
for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)
proof
let G be Group; ::_thesis: for a being Element of G
for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)
let a be Element of G; ::_thesis: for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)
defpred S1[ FinSequence of INT ] means  Product (((len $1) |-> a) |^ $1) = a |^ (Sum $1);
A1: for p being FinSequence of INT
for x being Element of INT st S1[p] holds
S1[p ^ <*x*>] by Lm3;
A2: S1[ <*> INT] by Lm2;
 for p being FinSequence of INT holds S1[p] from FINSEQ_2:sch_2(A2, A1);
hence  for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I) ; ::_thesis: verum
end;

theorem Th5: :: GR_CY_1:5
for G being Group
for b, a being Element of G holds
( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )
proof
let G be Group; ::_thesis: for b, a being Element of G holds
( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )
let b, a be Element of G; ::_thesis: ( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )
A1: ( ex j1 being Integer st b = a |^ j1 implies b in gr {a} )
proof
given j1 being Integer such that A2: b = a |^ j1 ; ::_thesis: b in gr {a}
consider n being Element of NAT  such that
A3: ( j1 = n or j1 = - n ) by INT_1:2;
percases ( j1 = n or j1 = - n ) by A3;
supposeA4: j1 = n ; ::_thesis: b in gr {a}
 ex F being FinSequence of G ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b )
proof
take F = n |-> a; ::_thesis: ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b )
A5: len F = n by CARD_1:def_7
.= len (n |-> (@ 1)) by CARD_1:def_7 ;
Product (F |^ (n |-> (@ 1))) = Product (F |^ ((len F) |-> (@ 1))) by CARD_1:def_7
.= Product (n |-> a) by GROUP_4:25
.= b by A2, A4, GROUP_4:12 ;
hence  ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b ) by A5, FUNCOP_1:13; ::_thesis: verum
end;
hence  b in gr {a} by GROUP_4:28; ::_thesis: verum
end;
suppose j1 = - n ; ::_thesis: b in gr {a}
then A6: b " = a |^ (- (- n)) by A2, GROUP_1:36
.= a |^ n ;
 ex F being FinSequence of G ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " )
proof
take F = n |-> a; ::_thesis: ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " )
A7: len F = n by CARD_1:def_7
.= len (n |-> (@ 1)) by CARD_1:def_7 ;
Product (F |^ (n |-> (@ 1))) = Product (F |^ ((len F) |-> (@ 1))) by CARD_1:def_7
.= Product (n |-> a) by GROUP_4:25
.= b " by A6, GROUP_4:12 ;
hence  ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " ) by A7, FUNCOP_1:13; ::_thesis: verum
end;
then  b " in gr {a} by GROUP_4:28;
then  (b ") " in gr {a} by GROUP_2:51;
hence  b in gr {a} ; ::_thesis: verum
end;
end;
end;
 ( b in gr {a} implies ex j1 being Integer st b = a |^ j1 )
proof
assume  b in gr {a} ; ::_thesis: ex j1 being Integer st b = a |^ j1
then consider F being FinSequence of G, I being FinSequence of INT  such that
A8: len F = len I and
A9: rng F c= {a} and
A10: Product (F |^ I) = b by GROUP_4:28;
take  Sum I ; ::_thesis: b = a |^ (Sum I)
A11: for p being Nat st p in dom F holds
F . p = ((len F) |-> a) . p
proof
let p be Nat; ::_thesis: ( p in dom F implies F . p = ((len F) |-> a) . p )
A12: dom F = Seg (len F) by FINSEQ_1:def_3;
assume A13: p in dom F ; ::_thesis: F . p = ((len F) |-> a) . p
then  F . p in rng F by FUNCT_1:def_3;
then F . p = a by A9, TARSKI:def_1
.= ((len F) |-> a) . p by A12, A13, FUNCOP_1:7 ;
hence  F . p = ((len F) |-> a) . p ; ::_thesis: verum
end;
dom ((len F) |-> a) = Seg (len F) by FUNCOP_1:13
.= dom F by FINSEQ_1:def_3 ;
then b = Product (((len I) |-> a) |^ I) by A8, A10, A11, FINSEQ_1:13
.= a |^ (Sum I) by Th4 ;
hence  b = a |^ (Sum I) ; ::_thesis: verum
end;
hence  ( b in gr {a} iff ex j1 being Integer st b = a |^ j1 ) by A1; ::_thesis: verum
end;

theorem Th6: :: GR_CY_1:6
for G being finite Group
for a being Element of G holds not a is being_of_order_0
proof
let G be finite Group; ::_thesis: for a being Element of G holds not a is being_of_order_0
let a be Element of G; ::_thesis: not a is being_of_order_0
 ex n being Nat st
( n <> 0 & a |^ n = 1_ G )
proof
deffunc H1( Nat) ->  Element of the carrier of G = a |^ $1;
consider F being FinSequence such that
A1: len F = (card G) + 1 and
A2: for p being Nat st p in dom F holds
F . p = H1(p) from FINSEQ_1:sch_2();
A3: dom F = Seg ((card G) + 1) by A1, FINSEQ_1:def_3;
A4: for y being set st y in rng F holds
ex n being Nat st y = a |^ n
proof
let y be set ; ::_thesis: ( y in rng F implies ex n being Nat st y = a |^ n )
assume  y in rng F ; ::_thesis: ex n being Nat st y = a |^ n
then consider x being set  such that
A5: x in dom F and
A6: F . x = y by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A5;
take  n ; ::_thesis: y = a |^ n
thus  y = a |^ n by A2, A5, A6; ::_thesis: verum
end;
 for x being set st x in rng F holds
x in the carrier of G
proof
let y be set ; ::_thesis: ( y in rng F implies y in the carrier of G )
assume  y in rng F ; ::_thesis: y in the carrier of G
then  ex n being Nat st y = a |^ n by A4;
hence  y in the carrier of G ; ::_thesis: verum
end;
then  rng F c= the carrier of G by TARSKI:def_3;
then reconsider F9 = F as Function of (Seg ((card G) + 1)), the carrier of G by A3, FUNCT_2:def_1, RELSET_1:4;
A7: card G < (card G) + 1 by XREAL_1:29;
 ( card (card G) = card the carrier of G & card (Seg ((card G) + 1)) = card ((card G) + 1) ) by FINSEQ_1:55;
then  card the carrier of G in card (Seg ((card G) + 1)) by A7, NAT_1:41;
then consider x, y being set  such that
A8: x in Seg ((card G) + 1) and
A9: y in Seg ((card G) + 1) and
A10: x <> y and
A11: F9 . x = F9 . y by FINSEQ_4:65;
reconsider p = x, n = y as Element of NAT by A8, A9;
percases ( n > p or p > n ) by A10, XXREAL_0:1;
supposeA12: n > p ; ::_thesis: ex n being Nat st
( n <> 0 & a |^ n = 1_ G )
then reconsider t = n - p as Element of NAT by INT_1:5;
take  t ; ::_thesis: ( t <> 0 & a |^ t = 1_ G )
 F9 . p = a |^ p by A2, A3, A8;
then  a |^ n = a |^ p by A2, A3, A9, A11;
then  a |^ (n + (- p)) = (a |^ p) * (a |^ (- p)) by GROUP_1:33;
then  a |^ t = a |^ (p + (- p)) by GROUP_1:33;
hence  ( t <> 0 & a |^ t = 1_ G ) by A12, GROUP_1:25; ::_thesis: verum
end;
supposeA13: p > n ; ::_thesis: ex n being Nat st
( n <> 0 & a |^ n = 1_ G )
then reconsider t = p - n as Element of NAT by INT_1:5;
take  t ; ::_thesis: ( t <> 0 & a |^ t = 1_ G )
 F9 . p = a |^ p by A2, A3, A8;
then  a |^ n = a |^ p by A2, A3, A9, A11;
then  a |^ (p + (- n)) = (a |^ n) * (a |^ (- n)) by GROUP_1:33;
then  a |^ t = a |^ (n + (- n)) by GROUP_1:33;
hence  ( t <> 0 & a |^ t = 1_ G ) by A13, GROUP_1:25; ::_thesis: verum
end;
end;
end;
hence  not a is being_of_order_0 by GROUP_1:def_10; ::_thesis: verum
end;

theorem Th7: :: GR_CY_1:7
for G being finite Group
for a being Element of G holds ord a = card (gr {a})
proof
let G be finite Group; ::_thesis: for a being Element of G holds ord a = card (gr {a})
let a be Element of G; ::_thesis: ord a = card (gr {a})
deffunc H1( Nat) ->  Element of the carrier of G = a |^ $1;
consider F being FinSequence such that
A1: len F = ord a and
A2: for p being Nat st p in dom F holds
F . p = H1(p) from FINSEQ_1:sch_2();
A3: dom F = Seg (ord a) by A1, FINSEQ_1:def_3;
A4: for y being set st y in rng F holds
ex n being Nat st y = a |^ n
proof
let y be set ; ::_thesis: ( y in rng F implies ex n being Nat st y = a |^ n )
assume  y in rng F ; ::_thesis: ex n being Nat st y = a |^ n
then consider x being set  such that
A5: x in dom F and
A6: F . x = y by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A5;
take  n ; ::_thesis: y = a |^ n
thus  y = a |^ n by A2, A5, A6; ::_thesis: verum
end;
 for x being set st x in rng F holds
x in the carrier of (gr {a})
proof
let y be set ; ::_thesis: ( y in rng F implies y in the carrier of (gr {a}) )
assume  y in rng F ; ::_thesis: y in the carrier of (gr {a})
then  ex n being Nat st y = a |^ n by A4;
then  y in gr {a} by Th5;
hence  y in the carrier of (gr {a}) by STRUCT_0:def_5; ::_thesis: verum
end;
then A7: rng F c= the carrier of (gr {a}) by TARSKI:def_3;
 not a is being_of_order_0 by Th6;
then A8: ord a <> 0 by GROUP_1:def_11;
A9: ex x being set st
( x in dom F & F . x = a )
proof
set x9 = 1;
 (ord a) + 1 > 0 + 1 by A8, XREAL_1:6;
then  ord a >= 1 by NAT_1:13;
then A10: 1 in dom F by A3;
then F . 1 = a |^ 1 by A2
.= a by GROUP_1:26 ;
hence  ex x being set st
( x in dom F & F . x = a ) by A10; ::_thesis: verum
end;
then A11: a in rng F by FUNCT_1:def_3;
 the carrier of (gr {a}) c= rng F
proof
 ex H being strict Subgroup of G st the carrier of H = rng F
proof
reconsider car = rng F as non empty set by A9, FUNCT_1:def_3;
 the carrier of (gr {a}) c= the carrier of G by GROUP_2:def_5;
then A12: car c= the carrier of G by A7, XBOOLE_1:1;
 dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1;
then A13: dom ( the multF of G || car) = [:car,car:] by A12, RELAT_1:62, ZFMISC_1:96;
 for y being set st y in rng ( the multF of G || car) holds
y in car
proof
let y be set ; ::_thesis: ( y in rng ( the multF of G || car) implies y in car )
set f = the multF of G || car;
assume  y in rng ( the multF of G || car) ; ::_thesis: y in car
then consider x being set  such that
A14: x in dom ( the multF of G || car) and
A15: ( the multF of G || car) . x = y by FUNCT_1:def_3;
consider xp, yp being set  such that
A16: [xp,yp] = x by A13, A14, RELAT_1:def_1;
 yp in car by A13, A14, A16, ZFMISC_1:87;
then consider s being Nat such that
A17: yp = a |^ s by A4;
 xp in car by A13, A14, A16, ZFMISC_1:87;
then consider p being Nat such that
A18: xp = a |^ p by A4;
A19: ex x being set st
( x in dom F & F . x = a |^ (p + s) )
proof
set t = (p + s) mod (ord a);
A20: (p + s) mod (ord a) < ord a by A8, NAT_D:1;
percases ( (p + s) mod (ord a) = 0 or (p + s) mod (ord a) > 0 ) ;
supposeA21: (p + s) mod (ord a) = 0 ; ::_thesis: ex x being set st
( x in dom F & F . x = a |^ (p + s) )
take  ord a ; ::_thesis: ( ord a in dom F & F . (ord a) = a |^ (p + s) )
a |^ (p + s) = a |^ (((ord a) * ((p + s) div (ord a))) + ((p + s) mod (ord a))) by A8, NAT_D:2
.= (a |^ ((ord a) * ((p + s) div (ord a)))) * (a |^ ((p + s) mod (ord a))) by GROUP_1:33
.= ((a |^ (ord a)) |^ ((p + s) div (ord a))) * (a |^ ((p + s) mod (ord a))) by GROUP_1:35
.= ((1_ G) |^ ((p + s) div (ord a))) * (a |^ ((p + s) mod (ord a))) by GROUP_1:41
.= (1_ G) * (a |^ ((p + s) mod (ord a))) by GROUP_1:31
.= a |^ 0 by A21, GROUP_1:def_4
.= 1_ G by GROUP_1:25
.= a |^ (ord a) by GROUP_1:41
.= F . (ord a) by A2, A3, A8, FINSEQ_1:3 ;
hence  ( ord a in dom F & F . (ord a) = a |^ (p + s) ) by A3, A8, FINSEQ_1:3; ::_thesis: verum
end;
suppose (p + s) mod (ord a) > 0 ; ::_thesis: ex x being set st
( x in dom F & F . x = a |^ (p + s) )
then  ((p + s) mod (ord a)) + 1 > 0 + 1 by XREAL_1:6;
then  (p + s) mod (ord a) >= 1 by NAT_1:13;
then A22: (p + s) mod (ord a) in dom F by A3, A20;
take  (p + s) mod (ord a) ; ::_thesis: ( (p + s) mod (ord a) in dom F & F . ((p + s) mod (ord a)) = a |^ (p + s) )
a |^ (p + s) = a |^ (((ord a) * ((p + s) div (ord a))) + ((p + s) mod (ord a))) by A8, NAT_D:2
.= (a |^ ((ord a) * ((p + s) div (ord a)))) * (a |^ ((p + s) mod (ord a))) by GROUP_1:33
.= ((a |^ (ord a)) |^ ((p + s) div (ord a))) * (a |^ ((p + s) mod (ord a))) by GROUP_1:35
.= ((1_ G) |^ ((p + s) div (ord a))) * (a |^ ((p + s) mod (ord a))) by GROUP_1:41
.= (1_ G) * (a |^ ((p + s) mod (ord a))) by GROUP_1:31
.= a |^ ((p + s) mod (ord a)) by GROUP_1:def_4 ;
hence  ( (p + s) mod (ord a) in dom F & F . ((p + s) mod (ord a)) = a |^ (p + s) ) by A2, A22; ::_thesis: verum
end;
end;
end;
y = (a |^ p) * (a |^ s) by A14, A15, A16, A18, A17, FUNCT_1:47
.= a |^ (p + s) by GROUP_1:33 ;
hence  y in car by A19, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng ( the multF of G || car) c= car by TARSKI:def_3;
then reconsider op = the multF of G || car as BinOp of car by A13, FUNCT_2:def_1, RELSET_1:4;
set H = multMagma(# car,op #);
A23: for f, g being Element of multMagma(# car,op #)
for f9, g9 being Element of G st f = f9 & g = g9 holds
f9 * g9 = f * g
proof
let f, g be Element of multMagma(# car,op #); ::_thesis: for f9, g9 being Element of G st f = f9 & g = g9 holds
f9 * g9 = f * g
let f9, g9 be Element of G; ::_thesis: ( f = f9 & g = g9 implies f9 * g9 = f * g )
A24: f * g = ( the multF of G || car) . [f,g] ;
assume  ( f = f9 & g = g9 ) ; ::_thesis: f9 * g9 = f * g
hence  f9 * g9 = f * g by A24, FUNCT_1:49; ::_thesis: verum
end;
A25: ex e being Element of multMagma(# car,op #) st
for h being Element of multMagma(# car,op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) )
proof
 ex x being set st
( x in dom F & F . x = a |^ (ord a) )
proof
set x9 = ord a;
 F . (ord a) = a |^ (ord a) by A2, A3, A8, FINSEQ_1:3;
hence  ex x being set st
( x in dom F & F . x = a |^ (ord a) ) by A3, A8, FINSEQ_1:3; ::_thesis: verum
end;
then  a |^ (ord a) in car by FUNCT_1:def_3;
then reconsider e = 1_ G as Element of multMagma(# car,op #) by GROUP_1:41;
take  e ; ::_thesis: for h being Element of multMagma(# car,op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) )
 for h being Element of multMagma(# car,op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) )
proof
let h be Element of multMagma(# car,op #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) )
reconsider h9 = h as Element of G by A12, TARSKI:def_3;
h * e = h9 * (1_ G) by A23
.= h9 by GROUP_1:def_4 ;
hence  h * e = h ; ::_thesis: ( e * h = h & ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) )
e * h = (1_ G) * h9 by A23
.= h9 by GROUP_1:def_4 ;
hence  e * h = h ; ::_thesis: ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e )
thus  ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) ::_thesis: verum
proof
 ex n being Nat st
( h = a |^ n & 1 <= n & ord a >= n )
proof
consider x being set  such that
A26: x in dom F and
A27: F . x = h by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A26;
take  n ; ::_thesis: ( h = a |^ n & 1 <= n & ord a >= n )
thus  ( h = a |^ n & 1 <= n & ord a >= n ) by A2, A3, A26, A27, FINSEQ_1:1; ::_thesis: verum
end;
then consider n being Nat such that
A28: h = a |^ n and
A29: ord a >= n ;
 ex x being set st
( x in dom F & F . x = a |^ ((ord a) - n) )
proof
percases ( ord a = n or ord a > n ) by A29, XXREAL_0:1;
supposeA30: ord a = n ; ::_thesis: ex x being set st
( x in dom F & F . x = a |^ ((ord a) - n) )
set x = ord a;
F . (ord a) = a |^ (ord a) by A2, A3, A8, FINSEQ_1:3
.= 1_ G by GROUP_1:41
.= a |^ ((ord a) - n) by A30, GROUP_1:25 ;
hence  ex x being set st
( x in dom F & F . x = a |^ ((ord a) - n) ) by A3, A8, FINSEQ_1:3; ::_thesis: verum
end;
supposeA31: ord a > n ; ::_thesis: ex x being set st
( x in dom F & F . x = a |^ ((ord a) - n) )
then reconsider x = (ord a) - n as Element of NAT by INT_1:5;
take  x ; ::_thesis: ( x in dom F & F . x = a |^ ((ord a) - n) )
 x in Seg (ord a)
proof
set r1 = ord a;
 ord a <= (ord a) + n by NAT_1:11;
then A32: x <= ord a by XREAL_1:20;
 (ord a) - n > n - n by A31, XREAL_1:9;
then  x >= 0 + 1 by NAT_1:13;
hence  x in Seg (ord a) by A32; ::_thesis: verum
end;
hence  ( x in dom F & F . x = a |^ ((ord a) - n) ) by A2, A3; ::_thesis: verum
end;
end;
end;
then reconsider g = a |^ ((ord a) - n) as Element of multMagma(# car,op #) by FUNCT_1:def_3;
A33: n + ((ord a) - n) = ord a ;
A34: g * h = (a |^ ((ord a) - n)) * (a |^ n) by A23, A28
.= a |^ (ord a) by A33, GROUP_1:33
.= e by GROUP_1:41 ;
h * g = (a |^ n) * (a |^ ((ord a) - n)) by A23, A28
.= a |^ (ord a) by A33, GROUP_1:33
.= e by GROUP_1:41 ;
hence  ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) by A34; ::_thesis: verum
end;
end;
hence  for h being Element of multMagma(# car,op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# car,op #) st
( h * g = e & g * h = e ) ) ; ::_thesis: verum
end;
 for f, g, h being Element of multMagma(# car,op #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# car,op #); ::_thesis: (f * g) * h = f * (g * h)
reconsider f9 = f, g9 = g, h9 = h as Element of G by A12, TARSKI:def_3;
A35: g * h = g9 * h9 by A23;
 f9 * g9 = f * g by A23;
then (f * g) * h = (f9 * g9) * h9 by A23
.= f9 * (g9 * h9) by GROUP_1:def_3
.= f * (g * h) by A23, A35 ;
hence  (f * g) * h = f * (g * h) ; ::_thesis: verum
end;
then reconsider H1 = multMagma(# car,op #) as Group by A25, GROUP_1:1;
 the carrier of (gr {a}) c= the carrier of G by GROUP_2:def_5;
then  the carrier of H1 c= the carrier of G by A7, XBOOLE_1:1;
then  H1 is Subgroup of G by GROUP_2:def_5;
hence  ex H being strict Subgroup of G st the carrier of H = rng F ; ::_thesis: verum
end;
then consider H being strict Subgroup of G such that
A36: the carrier of H = rng F ;
 {a} c= the carrier of H by A11, A36, ZFMISC_1:31;
then  gr {a} is Subgroup of H by GROUP_4:def_4;
hence  the carrier of (gr {a}) c= rng F by A36, GROUP_2:def_5; ::_thesis: verum
end;
then A37: rng F = the carrier of (gr {a}) by A7, XBOOLE_0:def_10;
reconsider So = Seg (ord a) as finite set ;
set ca = the carrier of (gr {a});
 F is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that
A38: x in dom F and
A39: y in dom F and
A40: F . x = F . y and
A41: x <> y ; ::_thesis: contradiction
reconsider s = y as Element of NAT by A39;
reconsider p = x as Element of NAT by A38;
A42: ( F . p = a |^ p & F . s = a |^ s ) by A2, A38, A39;
reconsider s9 = s, p9 = p, z = ord a as Real ;
percases ( p <= s or s <= p ) ;
suppose p <= s ; ::_thesis: contradiction
then reconsider r1 = s - p as Element of NAT by INT_1:5;
 p > 0 by A3, A38, FINSEQ_1:1;
then A43: z < z + p9 by XREAL_1:29;
 s9 <= z by A3, A39, FINSEQ_1:1;
then  s9 < z + p9 by A43, XXREAL_0:2;
then A44: s9 - p9 < (z + p9) - p9 by XREAL_1:9;
 1_ G = (a |^ s) * ((a |^ p) ") by A40, A42, GROUP_1:def_5;
then  a |^ 0 = (a |^ s) * ((a |^ p) ") by GROUP_1:25;
then  a |^ 0 = (a |^ s) * (a |^ (- p)) by GROUP_1:36;
then  a |^ 0 = a |^ (s + (- p)) by GROUP_1:33;
then A45: 1_ G = a |^ r1 by GROUP_1:25;
 ( r1 <> 0 & not a is being_of_order_0 ) by A41, Th6;
hence  contradiction by A45, A44, GROUP_1:def_11; ::_thesis: verum
end;
suppose s <= p ; ::_thesis: contradiction
then reconsider r2 = p - s as Element of NAT by INT_1:5;
 s > 0 by A3, A39, FINSEQ_1:1;
then A46: z < z + s9 by XREAL_1:29;
 p9 <= z by A3, A38, FINSEQ_1:1;
then  p9 < z + s9 by A46, XXREAL_0:2;
then A47: p9 - s9 < (z + s9) - s9 by XREAL_1:9;
 1_ G = (a |^ p) * ((a |^ s) ") by A40, A42, GROUP_1:def_5;
then  a |^ 0 = (a |^ p) * ((a |^ s) ") by GROUP_1:25;
then  a |^ 0 = (a |^ p) * (a |^ (- s)) by GROUP_1:36;
then  a |^ 0 = a |^ (p + (- s)) by GROUP_1:33;
then A48: 1_ G = a |^ r2 by GROUP_1:25;
 ( r2 <> 0 & not a is being_of_order_0 ) by A41, Th6;
hence  contradiction by A48, A47, GROUP_1:def_11; ::_thesis: verum
end;
end;
end;
then  Seg (ord a), the carrier of (gr {a}) are_equipotent by A3, A37, WELLORD2:def_4;
then  card So = card the carrier of (gr {a}) by CARD_1:5;
hence  ord a = card (gr {a}) by FINSEQ_1:57; ::_thesis: verum
end;

theorem Th8: :: GR_CY_1:8
for G being finite Group
for a being Element of G holds ord a divides card G
proof
let G be finite Group; ::_thesis: for a being Element of G holds ord a divides card G
let a be Element of G; ::_thesis: ord a divides card G
 ord a = card (gr {a}) by Th7;
hence  ord a divides card G by GROUP_2:148; ::_thesis: verum
end;

theorem Th9: :: GR_CY_1:9
for G being finite Group
for a being Element of G holds a |^ (card G) = 1_ G
proof
let G be finite Group; ::_thesis: for a being Element of G holds a |^ (card G) = 1_ G
let a be Element of G; ::_thesis: a |^ (card G) = 1_ G
 ord a divides card G by Th8;
then consider t being Nat such that
A1: card G = (ord a) * t by NAT_D:def_3;
a |^ (card G) = (a |^ (ord a)) |^ t by A1, GROUP_1:35
.= (1_ G) |^ t by GROUP_1:41
.= 1_ G by GROUP_1:31 ;
hence  a |^ (card G) = 1_ G ; ::_thesis: verum
end;

theorem Th10: :: GR_CY_1:10
for n being Nat
for G being finite Group
for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))
proof
let n be Nat; ::_thesis: for G being finite Group
for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))
let G be finite Group; ::_thesis: for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))
let a be Element of G; ::_thesis: (a |^ n) " = a |^ ((card G) - (n mod (card G)))
set q = card G;
set p9 = n mod (card G);
 n mod (card G) <= card G by NAT_D:1;
then reconsider q9 = (card G) - (n mod (card G)) as Element of NAT by INT_1:5;
(a |^ n) * (a |^ ((card G) - (n mod (card G)))) = a |^ (n + q9) by GROUP_1:33
.= a |^ ((((card G) * (n div (card G))) + (n mod (card G))) + q9) by NAT_D:2
.= a |^ ((((card G) * (n div (card G))) + (card G)) + ((- (n mod (card G))) + (n mod (card G))))
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (a |^ ((- (n mod (card G))) + (n mod (card G)))) by GROUP_1:33
.= (a |^ (((card G) * (n div (card G))) + (card G))) * ((a |^ (- (n mod (card G)))) * (a |^ (n mod (card G)))) by GROUP_1:33
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (((a |^ (n mod (card G))) ") * (a |^ (n mod (card G)))) by GROUP_1:36
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (1_ G) by GROUP_1:def_5
.= a |^ ((card G) * ((n div (card G)) + 1)) by GROUP_1:def_4
.= (a |^ (card G)) |^ ((n div (card G)) + 1) by GROUP_1:35
.= (1_ G) |^ ((n div (card G)) + 1) by Th9
.= 1_ G by GROUP_1:31 ;
hence  (a |^ n) " = a |^ ((card G) - (n mod (card G))) by GROUP_1:12; ::_thesis: verum
end;

registration
let G be non empty associative multMagma ;
cluster multMagma(# the carrier of G, the multF of G #) ->  associative ;
coherence
 multMagma(# the carrier of G, the multF of G #) is associative
proof
set H = multMagma(# the carrier of G, the multF of G #);
let x, y, z be Element of multMagma(# the carrier of G, the multF of G #); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
thus  (x * y) * z = x * (y * z) by BINOP_1:def_3; ::_thesis: verum
end;
end;

registration
let G be Group;
cluster multMagma(# the carrier of G, the multF of G #) ->  Group-like ;
coherence
 multMagma(# the carrier of G, the multF of G #) is Group-like
proof
set H = multMagma(# the carrier of G, the multF of G #);
reconsider e = 1_ G as Element of multMagma(# the carrier of G, the multF of G #) ;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of multMagma(# the carrier of G, the multF of G #); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * h = e ) )
reconsider h9 = h as Element of G ;
thus h * e = h9 * (1_ G)
.= h by GROUP_1:def_4 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * h = e ) )
thus e * h = (1_ G) * h9
.= h by GROUP_1:def_4 ; ::_thesis: ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * h = e )
reconsider g = h9 " as Element of multMagma(# the carrier of G, the multF of G #) ;
take  g ; ::_thesis: ( h * g = e & g * h = e )
thus h * g = h9 * (h9 ")
.= e by GROUP_1:def_5 ; ::_thesis: g * h = e
thus g * h = (h9 ") * h9
.= e by GROUP_1:def_5 ; ::_thesis: verum
end;
end;

theorem Th11: :: GR_CY_1:11
for G being finite strict Group st card G > 1 holds
ex a being Element of G st a <> 1_ G
proof
let G be finite strict Group; ::_thesis: ( card G > 1 implies ex a being Element of G st a <> 1_ G )
assume that
A1: card G > 1 and
A2: for a being Element of G holds a = 1_ G ; ::_thesis: contradiction
 for a being Element of G holds a in (1). G
proof
let a be Element of G; ::_thesis: a in (1). G
 a = 1_ G by A2;
then  a in {(1_ G)} by TARSKI:def_1;
then  a in the carrier of ((1). G) by GROUP_2:def_7;
hence  a in (1). G by STRUCT_0:def_5; ::_thesis: verum
end;
then  multMagma(# the carrier of G, the multF of G #) = (1). G by GROUP_2:62;
hence  contradiction by A1, GROUP_2:69; ::_thesis: verum
end;

theorem :: GR_CY_1:12
for p being Nat
for G being finite strict Group st card G = p & p is prime holds
for H being strict Subgroup of G holds
( H = (1). G or H = G )
proof
let p be Nat; ::_thesis: for G being finite strict Group st card G = p & p is prime holds
for H being strict Subgroup of G holds
( H = (1). G or H = G )
let G be finite strict Group; ::_thesis: ( card G = p & p is prime implies for H being strict Subgroup of G holds
( H = (1). G or H = G ) )
assume that
A1: card G = p and
A2: p is prime ; ::_thesis: for H being strict Subgroup of G holds
( H = (1). G or H = G )
let H be strict Subgroup of G; ::_thesis: ( H = (1). G or H = G )
 card H divides p by A1, GROUP_2:148;
then  ( card H = 1 or card H = p ) by A2, INT_2:def_4;
hence  ( H = (1). G or H = G ) by A1, GROUP_2:70, GROUP_2:73; ::_thesis: verum
end;

definition
func INT.Group  ->  non empty strict multMagma  equals :: GR_CY_1:def 3
 multMagma(# INT,addint #);
coherence
 multMagma(# INT,addint #) is non empty strict multMagma ;
end;

:: deftheorem  defines INT.Group GR_CY_1:def_3_:_
 INT.Group = multMagma(# INT,addint #);

registration
cluster INT.Group  ->  non empty strict Group-like associative ;
coherence
 ( INT.Group is associative & INT.Group is Group-like )
proof
set G = INT.Group ;
reconsider e = 0 as Element of INT.Group by INT_1:def_2;
thus  for h, g, f being Element of INT.Group holds (h * g) * f = h * (g * f) :: according to GROUP_1:def_3 ::_thesis: INT.Group is Group-like
proof
let h, g, f be Element of INT.Group; ::_thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Integer ;
A1: g * f = B + C by BINOP_2:def_20;
 h * g = A + B by BINOP_2:def_20;
hence (h * g) * f = (A + B) + C by BINOP_2:def_20
.= A + (B + C)
.= h * (g * f) by A1, BINOP_2:def_20 ;
::_thesis: verum
end;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of INT.Group holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of INT.Group st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of INT.Group; ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of INT.Group st
( h * b1 = e & b1 * h = e ) )
reconsider A = h as Integer ;
reconsider g = - A as Element of INT.Group ;
thus h * e = A + 0 by BINOP_2:def_20
.= h ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of INT.Group st
( h * b1 = e & b1 * h = e ) )
thus e * h = 0 + A by BINOP_2:def_20
.= h ; ::_thesis: ex b1 being Element of the carrier of INT.Group st
( h * b1 = e & b1 * h = e )
take  g ; ::_thesis: ( h * g = e & g * h = e )
thus h * g = A + (- A) by BINOP_2:def_20
.= e ; ::_thesis: g * h = e
thus g * h = (- A) + A by BINOP_2:def_20
.= e ; ::_thesis: verum
end;
end;

registration
cluster the carrier of INT.Group ->  integer-membered ;
coherence
 the carrier of INT.Group is integer-membered ;
end;

registration
let a, b be Element of INT.Group;
identifya * b with a + b;
compatibility
 a * b = a + b by BINOP_2:def_20;
end;

registration
let n be Nat;
cluster Segm n ->  natural-membered ;
coherence
 Segm n is natural-membered ;
end;

definition
let n be Nat;
assume A1: n > 0 ;
func addint n ->  BinOp of (Segm n) means :Def4: :: GR_CY_1:def 4
 for k, l being Element of Segm n holds it . (k,l) = (k + l) mod n;
existence
 ex b1 being BinOp of (Segm n) st
for k, l being Element of Segm n holds b1 . (k,l) = (k + l) mod n
proof
reconsider n = n as non zero Nat by A1;
defpred S1[ Nat, Nat, set ] means $3 = ($1 + $2) mod n;
A1: for k, l being Element of Segm n ex c being Element of Segm n st S1[k,l,c]
proof
let k, l be Element of Segm n; ::_thesis: ex c being Element of Segm n st S1[k,l,c]
 (k + l) mod n < n by NAT_D:1;
then reconsider c = (k + l) mod n as Element of Segm n by NAT_1:44;
take  c ; ::_thesis: S1[k,l,c]
thus  S1[k,l,c] ; ::_thesis: verum
end;
 ex o being BinOp of (Segm n) st
for a, b being Element of Segm n holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
hence  ex b1 being BinOp of (Segm n) st
for k, l being Element of Segm n holds b1 . (k,l) = (k + l) mod n ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b1 . (k,l) = (k + l) mod n ) & ( for k, l being Element of Segm n holds b2 . (k,l) = (k + l) mod n ) holds
b1 = b2
proof
let i1, i2 be BinOp of (Segm n); ::_thesis: ( ( for k, l being Element of Segm n holds i1 . (k,l) = (k + l) mod n ) & ( for k, l being Element of Segm n holds i2 . (k,l) = (k + l) mod n ) implies i1 = i2 )
assume that
A2: for k, l being Element of Segm n holds i1 . (k,l) = (k + l) mod n and
A3: for k, l being Element of Segm n holds i2 . (k,l) = (k + l) mod n ; ::_thesis: i1 = i2
 for k, l being Element of Segm n holds i1 . (k,l) = i2 . (k,l)
proof
let k, l be Element of Segm n; ::_thesis: i1 . (k,l) = i2 . (k,l)
thus i1 . (k,l) = (k + l) mod n by A2
.= i2 . (k,l) by A3 ; ::_thesis: verum
end;
hence  i1 = i2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines addint GR_CY_1:def_4_:_
 for n being Nat st n > 0 holds
for b2 being BinOp of (Segm n) holds
( b2 = addint n iff for k, l being Element of Segm n holds b2 . (k,l) = (k + l) mod n );

definition
let n be non zero Nat;
func INT.Group n ->  non empty strict multMagma  equals :: GR_CY_1:def 5
 multMagma(# (Segm n),(addint n) #);
coherence
 multMagma(# (Segm n),(addint n) #) is non empty strict multMagma ;
end;

:: deftheorem  defines INT.Group GR_CY_1:def_5_:_
 for n being non zero Nat holds INT.Group n = multMagma(# (Segm n),(addint n) #);

registration
let n be non zero Nat;
cluster INT.Group n ->  non empty finite strict Group-like associative ;
coherence
 ( INT.Group n is finite & INT.Group n is associative & INT.Group n is Group-like )
proof
set G = INT.Group n;
thus  the carrier of (INT.Group n) is finite ; :: according to STRUCT_0:def_11 ::_thesis: ( INT.Group n is associative & INT.Group n is Group-like )
reconsider e = 0 as Element of (INT.Group n) by NAT_1:44;
thus  for h, g, f being Element of (INT.Group n) holds (h * g) * f = h * (g * f) :: according to GROUP_1:def_3 ::_thesis: INT.Group n is Group-like
proof
let h, g, f be Element of (INT.Group n); ::_thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Element of Segm n ;
A1: g * f = (B + C) mod n by Def4;
 h * g = (A + B) mod n by Def4;
hence (h * g) * f = (((A + B) mod n) + C) mod n by Def4
.= ((A + B) + C) mod n by NAT_D:22
.= (A + (B + C)) mod n
.= (A + ((B + C) mod n)) mod n by NAT_D:22
.= h * (g * f) by A1, Def4 ;
::_thesis: verum
end;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (INT.Group n) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (INT.Group n) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (INT.Group n); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (INT.Group n) st
( h * b1 = e & b1 * h = e ) )
reconsider A = h as Element of Segm n ;
A2: A < n by NAT_1:44;
then consider p being Nat such that
A3: n = A + p by NAT_1:10;
thus h * e = (A + 0) mod n by Def4
.= h by A2, NAT_D:24 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (INT.Group n) st
( h * b1 = e & b1 * h = e ) )
thus e * h = (0 + A) mod n by Def4
.= h by A2, NAT_D:24 ; ::_thesis: ex b1 being Element of the carrier of (INT.Group n) st
( h * b1 = e & b1 * h = e )
 p mod n < n by NAT_D:1;
then reconsider g = p mod n as Element of (INT.Group n) by NAT_1:44;
reconsider B = g as Element of Segm n ;
take  g ; ::_thesis: ( h * g = e & g * h = e )
A4: p <= n by A3, NAT_1:12;
thus  h * g = e ::_thesis: g * h = e
proof
percases ( p = n or p < n ) by A4, XXREAL_0:1;
supposeA5: p = n ; ::_thesis: h * g = e
h * g = (A + B) mod n by Def4
.= (0 * n) mod n by A3, A5, NAT_D:25
.= e by NAT_D:13 ;
hence  h * g = e ; ::_thesis: verum
end;
supposeA6: p < n ; ::_thesis: h * g = e
h * g = (A + B) mod n by Def4
.= n mod n by A3, A6, NAT_D:24
.= e by NAT_D:25 ;
hence  h * g = e ; ::_thesis: verum
end;
end;
end;
thus  g * h = e ::_thesis: verum
proof
percases ( p = n or p < n ) by A4, XXREAL_0:1;
suppose p = n ; ::_thesis: g * h = e
then g * h = ((n mod n) + 0) mod n by A3, Def4
.= (0 * n) mod n by NAT_D:25
.= e by NAT_D:13 ;
hence  g * h = e ; ::_thesis: verum
end;
supposeA7: p < n ; ::_thesis: g * h = e
g * h = (A + B) mod n by Def4
.= n mod n by A3, A7, NAT_D:24
.= e by NAT_D:25 ;
hence  g * h = e ; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th13: :: GR_CY_1:13
1_ INT.Group = 0
proof
reconsider e = 0 as Element of INT.Group by INT_1:def_2;
 for h being Element of INT.Group holds
( h * e = h & e * h = h ) ;
hence  1_ INT.Group = 0 by GROUP_1:4; ::_thesis: verum
end;

theorem Th14: :: GR_CY_1:14
for n being non zero Nat holds 1_ (INT.Group n) = 0
proof
let n be non zero Nat; ::_thesis: 1_ (INT.Group n) = 0
reconsider e = 0 as Element of Segm n by NAT_1:44;
reconsider e = e as Element of (INT.Group n) ;
 for h being Element of (INT.Group n) holds
( h * e = h & e * h = h )
proof
let h be Element of (INT.Group n); ::_thesis: ( h * e = h & e * h = h )
reconsider A = h as Element of Segm n ;
reconsider A = A as Element of NAT ;
A1: A < n by NAT_1:44;
A2: e * h = (0 + A) mod n by Def4
.= h by A1, NAT_D:24 ;
h * e = (A + 0) mod n by Def4
.= h by A1, NAT_D:24 ;
hence  ( h * e = h & e * h = h ) by A2; ::_thesis: verum
end;
hence  1_ (INT.Group n) = 0 by GROUP_1:4; ::_thesis: verum
end;

definition
let h be Integer;
func @' h ->  Element of INT.Group equals :: GR_CY_1:def 6
h;
coherence
 h is Element of INT.Group by INT_1:def_2;
end;

:: deftheorem  defines @' GR_CY_1:def_6_:_
 for h being Integer holds @' h = h;

theorem Th15: :: GR_CY_1:15
for h being Element of INT.Group holds h " = - h
proof
let h be Element of INT.Group; ::_thesis: h " = - h
reconsider g = - h as Element of INT.Group ;
 h * g = 1_ INT.Group by Th13;
hence  h " = - h by GROUP_1:12; ::_thesis: verum
end;

 Lm4:  for k being Nat holds (@' 1) |^ k = k
proof
let k be Nat; ::_thesis: (@' 1) |^ k = k
defpred S1[ Nat] means (@' 1) |^ $1 = $1;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  (@' 1) |^ k = k ; ::_thesis: S1[k + 1]
then  ((@' 1) |^ k) * (@' 1) = k + 1 ;
hence  S1[k + 1] by GROUP_1:34; ::_thesis: verum
end;
A2: S1[ 0 ] by Th13, GROUP_1:25;
 for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1);
hence  (@' 1) |^ k = k ; ::_thesis: verum
end;

theorem Th16: :: GR_CY_1:16
for j1 being Integer holds j1 = (@' 1) |^ j1
proof
let j1 be Integer; ::_thesis: j1 = (@' 1) |^ j1
consider k being Element of NAT  such that
A1: ( j1 = k or j1 = - k ) by INT_1:2;
percases ( j1 = k or j1 = - k ) by A1;
suppose j1 = k ; ::_thesis: j1 = (@' 1) |^ j1
hence  j1 = (@' 1) |^ j1 by Lm4; ::_thesis: verum
end;
supposeA2: j1 = - k ; ::_thesis: j1 = (@' 1) |^ j1
reconsider k9 = k as Integer ;
reconsider k9 = k9 as Element of INT.Group by INT_1:def_2;
(@' 1) |^ j1 = ((@' 1) |^ k) " by A2, GROUP_1:36
.= k9 " by Lm4
.= j1 by A2, Th15 ;
hence  j1 = (@' 1) |^ j1 ; ::_thesis: verum
end;
end;
end;

Lm5:  INT.Group = gr {(@' 1)}
proof
reconsider h = 1 as Element of INT by INT_1:def_2;
reconsider h = h as Element of INT.Group ;
 for G1 being Subgroup of INT.Group st {h} c= the carrier of G1 holds
(Omega). INT.Group is Subgroup of G1
proof
let G1 be Subgroup of INT.Group ; ::_thesis: ( {h} c= the carrier of G1 implies (Omega). INT.Group is Subgroup of G1 )
assume A1: {h} c= the carrier of G1 ; ::_thesis: (Omega). INT.Group is Subgroup of G1
 the carrier of ((Omega). INT.Group) c= the carrier of G1
proof
 h in {h} by TARSKI:def_1;
then reconsider h99 = h as Element of G1 by A1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((Omega). INT.Group) or x in the carrier of G1 )
assume that
A2: x in the carrier of ((Omega). INT.Group) and
A3: not x in the carrier of G1 ; ::_thesis: contradiction
reconsider x9 = x as Integer by A2;
 ( h99 |^ x9 in the carrier of G1 & h99 |^ x9 = h |^ x9 ) by GROUP_4:2;
hence  contradiction by A3, Th16; ::_thesis: verum
end;
hence  (Omega). INT.Group is Subgroup of G1 by GROUP_2:57; ::_thesis: verum
end;
then  for G1 being strict Subgroup of INT.Group st {h} c= the carrier of G1 holds
(Omega). INT.Group is Subgroup of G1 ;
hence  INT.Group = gr {(@' 1)} by GROUP_4:def_4; ::_thesis: verum
end;

definition
let IT be Group;
attrIT is cyclic  means :Def7: :: GR_CY_1:def 7
 ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a};
end;

:: deftheorem Def7 defines cyclic GR_CY_1:def_7_:_
 for IT being Group holds
( IT is cyclic iff ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a} );

registration
cluster non empty strict unital Group-like associative cyclic for multMagma ;
existence
 ex b1 being Group st
( b1 is strict & b1 is cyclic )
proof
 INT.Group is cyclic by Def7, Lm5;
hence  ex b1 being Group st
( b1 is strict & b1 is cyclic ) ; ::_thesis: verum
end;
end;

registration
let G be Group;
cluster (1). G ->  cyclic ;
coherence
 (1). G is cyclic
proof
 1_ G in {(1_ G)} by TARSKI:def_1;
then reconsider PG = 1_ G as Element of ((1). G) by GROUP_2:def_7;
take  PG ; :: according to GR_CY_1:def_7 ::_thesis: multMagma(# the carrier of ((1). G), the multF of ((1). G) #) = gr {PG}
 for G1 being Subgroup of (1). G st {PG} c= the carrier of G1 holds
(Omega). ((1). G) is Subgroup of G1
proof
let G1 be Subgroup of (1). G; ::_thesis: ( {PG} c= the carrier of G1 implies (Omega). ((1). G) is Subgroup of G1 )
assume  {PG} c= the carrier of G1 ; ::_thesis: (Omega). ((1). G) is Subgroup of G1
then  the carrier of ((Omega). ((1). G)) c= the carrier of G1 by GROUP_2:def_7;
hence  (Omega). ((1). G) is Subgroup of G1 by GROUP_2:57; ::_thesis: verum
end;
then  for G1 being strict Subgroup of (1). G st {PG} c= the carrier of G1 holds
(Omega). ((1). G) is Subgroup of G1 ;
hence  multMagma(# the carrier of ((1). G), the multF of ((1). G) #) = gr {PG} by GROUP_4:def_4; ::_thesis: verum
end;
end;

registration
cluster non empty finite strict unital Group-like associative cyclic for multMagma ;
existence
 ex b1 being Group st
( b1 is strict & b1 is finite & b1 is cyclic )
proof
take  (1). the Group ; ::_thesis: ( (1). the Group is strict & (1). the Group is finite & (1). the Group is cyclic )
thus  ( (1). the Group is strict & (1). the Group is finite & (1). the Group is cyclic ) ; ::_thesis: verum
end;
end;

theorem Th17: :: GR_CY_1:17
for G being Group holds
( G is cyclic Group iff ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 )
proof
let G be Group; ::_thesis: ( G is cyclic Group iff ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 )
thus  ( G is cyclic Group implies ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 ) ::_thesis: ( ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 implies G is cyclic Group )
proof
assume  G is cyclic Group ; ::_thesis: ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1
then consider a being Element of G such that
A1: multMagma(# the carrier of G, the multF of G #) = gr {a} by Def7;
take  a ; ::_thesis: for b being Element of G ex j1 being Integer st b = a |^ j1
 for b being Element of G ex j1 being Integer st b = a |^ j1
proof
let b be Element of G; ::_thesis: ex j1 being Integer st b = a |^ j1
 b in gr {a} by A1, STRUCT_0:def_5;
hence  ex j1 being Integer st b = a |^ j1 by Th5; ::_thesis: verum
end;
hence  for b being Element of G ex j1 being Integer st b = a |^ j1 ; ::_thesis: verum
end;
given a being Element of G such that A2: for b being Element of G ex j1 being Integer st b = a |^ j1 ; ::_thesis: G is cyclic Group
 for b being Element of G holds b in gr {a}
proof
let b be Element of G; ::_thesis: b in gr {a}
 ex j1 being Integer st b = a |^ j1 by A2;
hence  b in gr {a} by Th5; ::_thesis: verum
end;
then  multMagma(# the carrier of G, the multF of G #) = gr {a} by GROUP_2:62;
hence  G is cyclic Group by Def7; ::_thesis: verum
end;

theorem Th18: :: GR_CY_1:18
for G being finite Group holds
( G is cyclic iff ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n )
proof
let G be finite Group; ::_thesis: ( G is cyclic iff ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n )
thus  ( G is cyclic implies ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n ) ::_thesis: ( ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n implies G is cyclic )
proof
assume  G is cyclic ; ::_thesis: ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n
then consider a being Element of G such that
A1: for b being Element of G ex j2 being Integer st b = a |^ j2 by Th17;
take  a ; ::_thesis: for b being Element of G ex n being Nat st b = a |^ n
let b be Element of G; ::_thesis: ex n being Nat st b = a |^ n
consider j2 being Integer such that
A2: b = a |^ j2 by A1;
consider n being Element of NAT  such that
A3: ( j2 = n or j2 = - n ) by INT_1:2;
percases ( j2 = n or j2 = - n ) by A3;
suppose j2 = n ; ::_thesis: ex n being Nat st b = a |^ n
hence  ex n being Nat st b = a |^ n by A2; ::_thesis: verum
end;
supposeA4: j2 = - n ; ::_thesis: ex n being Nat st b = a |^ n
 n mod (card G) <= card G by NAT_D:1;
then reconsider q9 = (card G) - (n mod (card G)) as Element of NAT by INT_1:5;
take  q9 ; ::_thesis: b = a |^ q9
b = (a |^ n) " by A2, A4, GROUP_1:36
.= a |^ q9 by Th10 ;
hence  b = a |^ q9 ; ::_thesis: verum
end;
end;
end;
given a being Element of G such that A5: for b being Element of G ex n being Nat st b = a |^ n ; ::_thesis: G is cyclic
 for b being Element of G ex j2 being Integer st b = a |^ j2
proof
let b be Element of G; ::_thesis: ex j2 being Integer st b = a |^ j2
consider n being Nat such that
A6: b = a |^ n by A5;
reconsider n = n as Integer ;
take  n ; ::_thesis: b = a |^ n
thus  b = a |^ n by A6; ::_thesis: verum
end;
hence  G is cyclic by Th17; ::_thesis: verum
end;

theorem Th19: :: GR_CY_1:19
for G being finite Group holds
( G is cyclic iff ex a being Element of G st ord a = card G )
proof
let G be finite Group; ::_thesis: ( G is cyclic iff ex a being Element of G st ord a = card G )
thus  ( G is cyclic implies ex a being Element of G st ord a = card G ) ::_thesis: ( ex a being Element of G st ord a = card G implies G is cyclic )
proof
reconsider H = multMagma(# the carrier of G, the multF of G #) as Group ;
assume  G is cyclic ; ::_thesis: ex a being Element of G st ord a = card G
then consider a being Element of G such that
A1: multMagma(# the carrier of G, the multF of G #) = gr {a} by Def7;
take  a ; ::_thesis: ord a = card G
 ord a = card H by A1, Th7;
hence  ord a = card G ; ::_thesis: verum
end;
given a being Element of G such that A2: ord a = card G ; ::_thesis: G is cyclic
 ex a being Element of G st multMagma(# the carrier of G, the multF of G #) = gr {a}
proof
consider a being Element of G such that
A3: ord a = card G by A2;
take  a ; ::_thesis: multMagma(# the carrier of G, the multF of G #) = gr {a}
 card (gr {a}) = card G by A3, Th7;
hence  multMagma(# the carrier of G, the multF of G #) = gr {a} by GROUP_2:73; ::_thesis: verum
end;
hence  G is cyclic by Def7; ::_thesis: verum
end;

theorem :: GR_CY_1:20
for G being finite Group
for H being strict Subgroup of G st G is cyclic holds
H is cyclic
proof
let G be finite Group; ::_thesis: for H being strict Subgroup of G st G is cyclic holds
H is cyclic
let H be strict Subgroup of G; ::_thesis: ( G is cyclic implies H is cyclic )
A1: card H >= 1 by GROUP_1:45;
assume  G is cyclic ; ::_thesis: H is cyclic
then consider a being Element of G such that
A2: for b being Element of G ex n being Nat st b = a |^ n by Th18;
percases ( card H = 1 or card H > 1 ) by A1, XXREAL_0:1;
suppose card H = 1 ; ::_thesis: H is cyclic
then  H = (1). G by GROUP_2:70;
hence  H is cyclic ; ::_thesis: verum
end;
supposeA3: card H > 1 ; ::_thesis: H is cyclic
defpred S1[ Nat] means ( $1 > 0 & a |^ $1 is Element of H );
consider h being Element of H such that
A4: h <> 1_ H by A3, Th11;
 h is Element of G by GROUP_2:42;
then consider n being Nat such that
A5: h = a |^ n by A2;
 n <> 0
proof
assume  n = 0 ; ::_thesis: contradiction
then h = 1_ G by A5, GROUP_1:25
.= 1_ H by GROUP_2:44 ;
hence  contradiction by A4; ::_thesis: verum
end;
then A6: ex n being Nat st S1[n] by A5;
 ex h1 being Element of H st
for b being Element of H ex s being Nat st b = h1 |^ s
proof
 ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A6);
then consider n being Nat such that
A7: n > 0 and
A8: a |^ n is Element of H and
A9: for k being Nat st k > 0 & a |^ k is Element of H holds
n <= k ;
consider h1 being Element of H such that
A10: h1 = a |^ n by A8;
take  h1 ; ::_thesis: for b being Element of H ex s being Nat st b = h1 |^ s
 for b being Element of H ex s being Nat st b = h1 |^ s
proof
let b be Element of H; ::_thesis: ex s being Nat st b = h1 |^ s
 b is Element of G by GROUP_2:42;
then consider p being Nat such that
A11: b = a |^ p by A2;
consider s, r being Nat such that
A12: p = (n * s) + r and
A13: r < n by A7, NAT_1:17;
reconsider s = s, r = r as Element of NAT by ORDINAL1:def_12;
take  s ; ::_thesis: b = h1 |^ s
 r = 0
proof
 h1 |^ s = (a |^ n) |^ s by A10, GROUP_4:1;
then (h1 |^ s) " = ((a |^ n) |^ s) " by GROUP_2:48
.= (a |^ (n * s)) " by GROUP_1:35 ;
then reconsider g = (a |^ (n * s)) " as Element of H ;
reconsider b = a |^ p as Element of H by A11;
 a |^ p = (a |^ (n * s)) * (a |^ r) by A12, GROUP_1:33;
then ((a |^ (n * s)) ") * (a |^ p) = (((a |^ (n * s)) ") * (a |^ (n * s))) * (a |^ r) by GROUP_1:def_3
.= (1_ G) * (a |^ r) by GROUP_1:def_5
.= a |^ r by GROUP_1:def_4 ;
then A14: g * b = a |^ r by GROUP_2:43;
assume  r <> 0 ; ::_thesis: contradiction
hence  contradiction by A9, A13, A14; ::_thesis: verum
end;
then a |^ p = (a |^ n) |^ s by A12, GROUP_1:35
.= h1 |^ s by A10, GROUP_4:1 ;
hence  b = h1 |^ s by A11; ::_thesis: verum
end;
hence  for b being Element of H ex s being Nat st b = h1 |^ s ; ::_thesis: verum
end;
hence  H is cyclic by Th18; ::_thesis: verum
end;
end;
end;

theorem :: GR_CY_1:21
for G being finite strict Group st card G is prime holds
G is cyclic Group
proof
let G be finite strict Group; ::_thesis: ( card G is prime implies G is cyclic Group )
assume A1: card G is prime ; ::_thesis: G is cyclic Group
set p = card G;
 ex a being Element of G st ord a = card G
proof
assume A2: for a being Element of G holds ord a <> card G ; ::_thesis: contradiction
A3: now__::_thesis:_for_a_being_Element_of_G_holds_ord_a_=_1
let a be Element of G; ::_thesis: ord a = 1
 ord a divides card G by Th8;
then  ( ord a = 1 or ord a = card G ) by A1, INT_2:def_4;
hence  ord a = 1 by A2; ::_thesis: verum
end;
 for x being set st x in the carrier of G holds
x in the carrier of ((1). G)
proof
let x be set ; ::_thesis: ( x in the carrier of G implies x in the carrier of ((1). G) )
assume  x in the carrier of G ; ::_thesis: x in the carrier of ((1). G)
then reconsider x9 = x as Element of G ;
 ord x9 = 1 by A3;
then  x9 = 1_ G by GROUP_1:43;
then  x9 in {(1_ G)} by TARSKI:def_1;
hence  x in the carrier of ((1). G) by GROUP_2:def_7; ::_thesis: verum
end;
then  the carrier of G c= the carrier of ((1). G) by TARSKI:def_3;
then  G = (1). G by GROUP_2:61;
then  card G = 1 by GROUP_2:69;
hence  contradiction by A1, INT_2:def_4; ::_thesis: verum
end;
hence  G is cyclic Group by Th19; ::_thesis: verum
end;

theorem Th22: :: GR_CY_1:22
for n being non zero Nat ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1
proof
let n be non zero Nat; ::_thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1
 0 + 1 < n + 1 by XREAL_1:6;
then A1: n >= 1 by NAT_1:13;
now__::_thesis:_ex_g_being_Element_of_(INT.Group_n)_st_
for_b_being_Element_of_(INT.Group_n)_ex_j1_being_Integer_st_b_=_g_|^_j1
percases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;
suppose n = 1 ; ::_thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1
then  the carrier of (INT.Group n) = {(1_ (INT.Group n))} by Th14, CARD_1:49
.= the carrier of ((1). (INT.Group n)) by GROUP_2:def_7 ;
then  INT.Group n = (1). (INT.Group n) by GROUP_2:61;
hence  ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 by Th17; ::_thesis: verum
end;
suppose n > 1 ; ::_thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1
then reconsider g9 = 1 as Element of Segm n by NAT_1:44;
reconsider g = g9 as Element of (INT.Group n) ;
 for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1
proof
let b be Element of (INT.Group n); ::_thesis: ex j1 being Integer st b = g |^ j1
reconsider b9 = b as Element of NAT by Lm1;
defpred S1[ Nat] means g |^ $1 = $1 mod n;
A2: b9 < n by NAT_1:44;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: g |^ k = k mod n ; ::_thesis: S1[k + 1]
 k mod n < n by NAT_D:1;
then reconsider e = k mod n as Element of Segm n by NAT_1:44;
g |^ (k + 1) = (g |^ k) * (g |^ 1) by GROUP_1:33
.= (g |^ k) * g by GROUP_1:26
.= (e + g9) mod n by A4, Def4
.= (k + 1) mod n by NAT_D:22 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
g |^ 0 = 1_ (INT.Group n) by GROUP_1:25
.= 0 by Th14
.= 0 mod n by NAT_D:26 ;
then A5: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A5, A3);
then A6: g |^ b9 = b9 mod n
.= b by A2, NAT_D:24 ;
reconsider b9 = b9 as Integer ;
take  b9 ; ::_thesis: b = g |^ b9
thus  b = g |^ b9 by A6; ::_thesis: verum
end;
hence  ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 ; ::_thesis: verum
end;
end;
end;
hence  ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 ; ::_thesis: verum
end;

registration
cluster non empty Group-like associative cyclic  ->  commutative for multMagma ;
coherence
 for b1 being Group st b1 is cyclic holds
b1 is commutative
proof
let G be Group; ::_thesis: ( G is cyclic implies G is commutative )
assume A1: G is cyclic ; ::_thesis: G is commutative
 for a, b being Element of G holds a * b = b * a
proof
let a, b be Element of G; ::_thesis: a * b = b * a
 ex e being Element of G ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 )
proof
consider e being Element of G such that
A2: for d being Element of G ex j3 being Integer st d = e |^ j3 by A1, Th17;
take  e ; ::_thesis: ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 )
 ( ex j2 being Integer st a = e |^ j2 & ex j3 being Integer st b = e |^ j3 ) by A2;
hence  ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 ) ; ::_thesis: verum
end;
then consider e being Element of G, j2, j3 being Integer such that
A3: ( a = e |^ j2 & b = e |^ j3 ) ;
a * b = e |^ (j3 + j2) by A3, GROUP_1:33
.= b * a by A3, GROUP_1:33 ;
hence  a * b = b * a ; ::_thesis: verum
end;
hence  G is commutative by GROUP_1:def_12; ::_thesis: verum
end;
end;

theorem :: GR_CY_1:23
INT.Group = gr {(@' 1)} by Lm5;

registration
cluster INT.Group  ->  non empty strict cyclic ;
coherence
 INT.Group is cyclic
proof
take  @' 1 ; :: according to GR_CY_1:def_7 ::_thesis: multMagma(# the carrier of INT.Group, the multF of INT.Group #) = gr {(@' 1)}
thus  multMagma(# the carrier of INT.Group, the multF of INT.Group #) = gr {(@' 1)} by Lm5; ::_thesis: verum
end;
end;

registration
let n be non zero Nat;
cluster INT.Group n ->  non empty strict cyclic ;
coherence
 INT.Group n is cyclic
proof
 ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 by Th22;
hence  INT.Group n is cyclic by Th17; ::_thesis: verum
end;
end;