let p be Prime; :: thesis: ex g being Element of (GF p) st
for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n
consider g being Element of (MultGroup (GF p)) such that
A1: for a being Element of (MultGroup (GF p)) ex n being Nat st a = g |^ n by GR_CY_1:18;
reconsider g0 = g as Element of (GF p) by UNIROOTS:19;
take g0 ; :: thesis: for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g0 |^ n
now :: thesis: for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g0 |^ n
let a be Element of (GF p); :: thesis: ( a <> 0. (GF p) implies ex n being Nat st a = g0 |^ n )
assume a <> 0. (GF p) ; :: thesis: ex n being Nat st a = g0 |^ n
then A2: not a in {(0. (GF p))} by TARSKI:def 1;
the carrier of (GF p) = the carrier of (MultGroup (GF p)) \/ {(0. (GF p))} by UNIROOTS:15;
then reconsider a0 = a as Element of (MultGroup (GF p)) by A2, XBOOLE_0:def 3;
consider n being Nat such that
A3: a0 = g |^ n by A1;
take n = n; :: thesis: a = g0 |^ n
thus a = g0 |^ n by A3, Th29; :: thesis: verum
end;
hence for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g0 |^ n ; :: thesis: verum