let p be Prime; :: thesis: for L being Field
for n being Nat st 0 < n & L = INT.Ring p holds
ex f being Polynomial of L st
( deg f = n & ( 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)) ) )
let L be Field; :: thesis: for n being Nat st 0 < n & L = INT.Ring p holds
ex f being Polynomial of L st
( deg f = n & ( 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)) ) )
let n be Nat; :: thesis: ( 0 < n & L = INT.Ring p implies ex f being Polynomial of L st
( deg f = n & ( 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)) ) ) )
assume that
A1: 0 < n and
A2: L = INT.Ring p ; :: thesis: ex f being Polynomial of L st
( deg f = n & ( 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)) ) )
set qq = 1_. L;
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set f = (<%(0. L),(1. L)%> `^ n0) - (1_. L);
set pp = <%(0. L),(1. L)%> `^ n0;

A3: now :: thesis: 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 (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))

let x be Element of L; :: thesis: for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))
let xz be Element of (Z/Z* p); :: thesis: for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))
let xn be Element of (INT.Ring p); :: thesis: ( x = xz & xn = xz |^ n implies eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p)) )
assume that
A4: x = xz and
A5: xn = xz |^ n ; :: thesis: eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))
A6: xn = xz |^ n0 by A5
.= (power L) . (x,n0) by A2, A4, Th28 ;
thus eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = (eval ((<%(0. L),(1. L)%> `^ n0),x)) - (eval ((1_. L),x)) by POLYNOM4:21
.= (eval ((<%(0. L),(1. L)%> `^ n0),x)) - (1. L) by POLYNOM4:18
.= ((power L) . ((eval (<%(0. L),(1. L)%>,x)),n0)) - (1. L) by POLYNOM5:22
.= xn - (1_ (INT.Ring p)) by A2, A6, POLYNOM5:48 ; :: thesis: verum

end;

A7: len (1_. L) = 1 by POLYNOM4:4;
len <%(0. L),(1. L)%> = 2 by POLYNOM5:40;
then A8: len (<%(0. L),(1. L)%> `^ n0) = ((n * 2) - n) + 1 by POLYNOM5:23
.= n + 1 ;
A9: 0 + 1 < n + 1 by A1, XREAL_1:8;
then len (<%(0. L),(1. L)%> `^ n0) <> len (- (1_. L)) by A8, A7, POLYNOM4:8;
then len ((<%(0. L),(1. L)%> `^ n0) - (1_. L)) = max ((len (<%(0. L),(1. L)%> `^ n0)),(len (- (1_. L)))) by POLYNOM4:7
.= max ((n + 1),1) by A8, A7, POLYNOM4:8
.= n + 1 by A9, XXREAL_0:def 10 ;
then deg ((<%(0. L),(1. L)%> `^ n0) - (1_. L)) = n ;
hence ex f being Polynomial of L st
( deg f = n & ( 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 A3; :: thesis: verum