let p be Prime; :: thesis: for F being p -characteristic Field
for q being Element of the carrier of (Polynom-Ring F) st ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) holds
ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q
let F be p -characteristic Field; :: thesis: for q being Element of the carrier of (Polynom-Ring F) st ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) holds
ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q
let q be Element of the carrier of (Polynom-Ring F); :: thesis: ( ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) implies ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q )
assume AS: for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ; :: thesis: ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q

per cases ( q is zero or not q is zero ) ;

suppose q is zero ; :: thesis: ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q

then H: q = 0_. F by UPROOTS:def 5
.= 0. (Polynom-Ring F) by POLYNOM3:def 10 ;
then q |^ p = 0. (Polynom-Ring F) ;
hence ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q by H; :: thesis: verum

end;

suppose not q is zero ; :: thesis: ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q

then reconsider q = q as non zero Element of the carrier of (Polynom-Ring F) ;
defpred S₁[ Nat] means for q being non zero Element of the carrier of (Polynom-Ring F) st deg q = $1 * p & ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) holds
ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q;

IS: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume IV: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for q being non zero Element of the carrier of (Polynom-Ring F) st deg q = k * p & ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) holds
ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q

let q be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( deg q = k * p & ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) implies ex r being Element of the carrier of (Polynom-Ring F) st b₂ |^ p = r )
assume A1: ( deg q = k * p & ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) ) ; :: thesis: ex r being Element of the carrier of (Polynom-Ring F) st b₂ |^ p = r
H: q <> 0_. F ;
then len q <> 0 by POLYNOM4:5;
then K: (len q) -' 1 = (len q) - 1 by XREAL_0:def 2;
consider r being Polynomial of F such that
A2: ( len r < len q & q = r + (LM q) & ( for n being Element of NAT st n < (len q) - 1 holds
r . n = q . n ) ) by H, POLYNOM4:5, POLYNOM4:16;
not LC q is zero ;
then J: q . ((len q) - 1) <> 0. F by K, RATFUNC1:def 6;
then q . (deg q) <> 0. F by HURWITZ:def 2;
then deg q in Support q by POLYNOM1:def 4;
then consider b being Element of F such that
A4: b |^ p = q . (deg q) by A1;
reconsider r1 = anpoly (b,k) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
K: not b is zero by A4, J, HURWITZ:def 2;
A5: LM q = anpoly ((b |^ p),(k * p)) by A4, A1, FIELD_1:11
.= (anpoly (b,k)) `^ p by K, DP3
.= r1 |^ p ;

per cases ( r is zero or not r is zero ) ;

suppose r is zero ; :: thesis: ex r being Element of the carrier of (Polynom-Ring F) st b₂ |^ p = r

hence ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q by A2, A5; :: thesis: verum

end;

suppose not r is zero ; :: thesis: ex r being Element of the carrier of (Polynom-Ring F) st b₂ |^ p = r

then reconsider r = r as non zero Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
r <> 0_. F ;
then len r <> 0 by POLYNOM4:5;
then K: (len r) -' 1 = (len r) - 1 by XREAL_0:def 2;

H: now :: thesis: for i being Element of NAT st i in Support r holds
( r . i = q . i & i in Support q )

let i be Element of NAT ; :: thesis: ( i in Support r implies ( r . i = q . i & i in Support q ) )
assume i in Support r ; :: thesis: ( r . i = q . i & i in Support q )
then H1: r . i <> 0. F by POLYNOM1:def 4;

now :: thesis: not i >= (len q) - 1

assume H2: i >= (len q) - 1 ; :: thesis: contradiction
(len q) - 1 > (len r) - 1 by A2, XREAL_1:9;
then i > (len r) - 1 by H2, XXREAL_0:2;
then i >= ((len r) - 1) + 1 by INT_1:7;
hence contradiction by H1, ALGSEQ_1:8; :: thesis: verum

end;

hence r . i = q . i by A2; :: thesis: i in Support q
hence i in Support q by H1, POLYNOM1:def 4; :: thesis: verum

end;

not LC r is zero ;
then r . ((len r) - 1) <> 0. F by K, RATFUNC1:def 6;
then r . (deg r) <> 0. F by HURWITZ:def 2;
then deg r in Support r by POLYNOM1:def 4;
then deg r in Support q by H;
then consider k1 being Nat such that
A6: deg r = p * k1 by A1, NAT_D:def 3;
(len r) - 1 < (len q) - 1 by A2, XREAL_1:9;
then deg r < (len q) - 1 by HURWITZ:def 2;
then deg r < deg q by HURWITZ:def 2;
then (p * k1) / p < (p * k) / p by A1, A6, XREAL_1:74;
then k1 * (p / p) < (p * k) / p ;
then k1 * 1 < k * (p / p) by XCMPLX_1:60;
then A7: k1 < k * 1 by XCMPLX_1:60;

now :: thesis: for i being Nat st i in Support r holds
( p divides i & ex a being Element of F st a |^ p = r . i )

let i be Nat; :: thesis: ( i in Support r implies ( p divides i & ex a being Element of F st a |^ p = r . i ) )
assume K: i in Support r ; :: thesis: ( p divides i & ex a being Element of F st a |^ p = r . i )
then L: i in Support q by H;
hence p divides i by A1; :: thesis: ex a being Element of F st a |^ p = r . i
consider a being Element of F such that
M: a |^ p = q . i by L, A1;
r . i = a |^ p by M, K, H;
hence ex a being Element of F st a |^ p = r . i ; :: thesis: verum

end;

then consider r2 being Element of the carrier of (Polynom-Ring F) such that
A8: r2 |^ p = r by A6, A7, IV;
(r1 + r2) |^ p = (r1 |^ p) + (r2 |^ p) by fresh
.= q by A2, A5, A8, POLYNOM3:def 10 ;
hence ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q ; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(IS);
not LC q is zero ;
then q . ((len q) -' 1) <> 0. F by RATFUNC1:def 6;
then (len q) -' 1 in Support q by POLYNOM1:def 4;
then consider k being Nat such that
H: (len q) -' 1 = p * k by AS, NAT_D:def 3;
q <> 0_. F ;
then len q <> 0 by POLYNOM4:5;
then (len q) -' 1 = (len q) - 1 by XREAL_0:def 2;
then deg q = (len q) -' 1 by HURWITZ:def 2;
hence ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q by AS, H, I; :: thesis: verum

end;

end;