let p be Prime; :: thesis: for L being Field
for n being natural number 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 natural number 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 natural number ; :: 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 13;
set f = (<%(0. L),(1. L)%> `^ n0) - (1_. L);
set pp = <%(0. L),(1. L)%> `^ n0;

A3: now

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:24
.= (eval ((<%(0. L),(1. L)%> `^ n0),x)) - (1. L) by POLYNOM4:21
.= ((power L) . ((eval (<%(0. L),(1. L)%>,x)),n0)) - (1. L) by POLYNOM5:23
.= xn - (1_ (INT.Ring p)) by A2, A6, POLYNOM5:49 ; :: thesis: verum

end;

A7: len (1_. L) = 1 by POLYNOM4:7;
len <%(0. L),(1. L)%> = 2 by POLYNOM5:41;
then A8: len (<%(0. L),(1. L)%> `^ n0) = ((n * 2) - n) + 1 by POLYNOM5:24
.= n + 1 ;
A9: 0 + 1 < n + 1 by A1, XREAL_1:10;
then len (<%(0. L),(1. L)%> `^ n0) <> len (- (1_. L)) by A8, A7, POLYNOM4:11;
then len ((<%(0. L),(1. L)%> `^ n0) - (1_. L)) = max ((len (<%(0. L),(1. L)%> `^ n0)),(len (- (1_. L)))) by POLYNOM4:10
.= max ((n + 1),1) by A8, A7, POLYNOM4:11
.= 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