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 A1: ( 0 < n & 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)) ) )
A2: 0 + 1 < n + 1 by A1, XREAL_1:10;
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;
set qq = 1_. L;

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 A4: ( x = xz & xn = xz |^ n ) ; :: thesis: eval ((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x = xn - (1_ (INT.Ring p))
A5: xn = xz |^ n0 by A4
.= (power L) . x,n0 by A1, 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 A1, A5, POLYNOM5:49 ; :: thesis: verum

end;

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