let p be Prime; :: thesis:
let a, b be Element of (Z/Z* p); :: thesis:
let n be Nat; :: thesis:
assume that
A1: 0 < n and
A2: ord a = n and
A3: b |^ n = 1 ; :: thesis:
reconsider XX = the carrier of (gr {a}) as finite set ;
A4: ex D being finite set st
( D = the carrier of (gr {a}) & card (gr {a}) = card D ) ;
reconsider L = INT.Ring p as non empty unital doubleLoopStr ;
consider f being Polynomial of L such that
A5: deg f = n and
A6: for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) by A1, Lm14;
consider m, n0 being Element of NAT such that
A7: n0 = deg f and
A8: m = card (Roots f) and
A9: m <= n0 by A5, Th27;
assume b is not Element of (gr {a}) ; :: thesis:
then card ( the carrier of (gr {a}) \/ {b}) = (card XX) + 1 by CARD_2:41
.= n0 + 1 by A2, A5, A7, A4, GR_CY_1:7 ;
then A10: card (n0 + 1) = card ( the carrier of (gr {a}) \/ {b}) ;
A11: 1 < p by INT_2:def 4;
A12: for x being Element of (Z/Z* p) st x |^ n = 1 holds
x in Roots f

let x1 be Element of (Z/Z* p); :: thesis:
assume x1 |^ n = 1 ; :: thesis:
then A13: x1 |^ n = 1_ (Z/Z* p) by Th21
.= 1_ (INT.Ring p) by Th21 ;
x1 |^ n in Segm0 p ;
then x1 |^ n in (Segm p) \ {0} by A11, Def2;
then reconsider x2 = x1 |^ n as Element of (INT.Ring p) by XBOOLE_0:def 5;
x1 in Segm0 p ;
then x1 in (Segm p) \ {0} by A11, Def2;
then reconsider x3 = x1 as Element of L by XBOOLE_0:def 5;
eval (f,x3) = x2 - (1_ (INT.Ring p)) by A6
.= 0. L by A13, RLVECT_1:15 ;
then x3 is_a_root_of f by POLYNOM5:def 7;
hence x1 in Roots f by POLYNOM5:def 10; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in the carrier of (gr {a}) ; :: thesis:
then x in gr {a} ;
then x in Z/Z* p by GROUP_2:40;
then reconsider x1 = x as Element of (Z/Z* p) ;
x1 in gr {a} by A15;
then consider j being Integer such that
A16: x1 = a |^ j by GR_CY_1:5;
x1 |^ n = a |^ (j * n) by A16, GROUP_1:35
.= (a |^ n) |^ j by GROUP_1:35
.= (1_ (Z/Z* p)) |^ j by A2, GROUP_1:41
.= 1_ (Z/Z* p) by GROUP_1:31
.= 1 by Th21 ;
hence x in Roots f by A12; :: thesis:

end;