let p be Prime; :: thesis: for x being Element of (MultGroup (GF p))
for x1 being Element of (GF p)
for n being Nat st x = x1 holds
x |^ n = x1 |^ n
let x be Element of (MultGroup (GF p)); :: thesis: for x1 being Element of (GF p)
for n being Nat st x = x1 holds
x |^ n = x1 |^ n
let x1 be Element of (GF p); :: thesis: for n being Nat st x = x1 holds
x |^ n = x1 |^ n
let n be Nat; :: thesis: ( x = x1 implies x |^ n = x1 |^ n )
assume A1: x = x1 ; :: thesis: x |^ n = x1 |^ n
defpred S1[ Nat] means x |^ $1 = x1 |^ $1;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A3: x |^ (n + 1) = (x |^ n) * x by GROUP_1:34;
A4: x1 |^ (n + 1) = (x1 |^ n) * x1 by Th24;
assume x |^ n = x1 |^ n ; :: thesis: S1[n + 1]
hence S1[n + 1] by A1, A3, A4, UNIROOTS:16; :: thesis: verum
end;
x |^ 0 = 1_ (MultGroup (GF p)) by GROUP_1:25
.= 1_ (GF p) by UNIROOTS:17
.= x1 |^ 0 by Th21 ;
then A5: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A5, A2);
 hence x |^ n = x1 |^ n ; :: thesis: verum