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
P1: 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

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 P0: 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 P0, XBOOLE_0:def 3;
consider n being Nat such that
P2: a0 = g |^ n by P1;
take n = n; :: thesis: a = g0 |^ n
thus a = g0 |^ n by P2, LMCycle4; :: 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