let p be Prime; :: thesis: for F being p -characteristic Field
for a, b being Element of F st b |^ p = a holds
X^ (p,a) = (X- b) |^ p
let R be p -characteristic Field; :: thesis: for a, b being Element of R st b |^ p = a holds
X^ (p,a) = (X- b) |^ p
let a, b be Element of R; :: thesis: ( b |^ p = a implies X^ (p,a) = (X- b) |^ p )
assume AS: b |^ p = a ; :: thesis: X^ (p,a) = (X- b) |^ p

per cases ( p = 2 or p <> 2 ) ;

suppose C: p = 2 ; :: thesis: X^ (p,a) = (X- b) |^ p

then D: (X- b) |^ p = <%(- b),(1. R)%> `^ 2 by RING_5:10
.= <%(- b),(1. R)%> *' <%(- b),(1. R)%> by POLYNOM5:17
.= <%((- b) * (- b)),(((- b) * (1. R)) + ((1. R) * (- b))),((1. R) * (1. R))%> by FIELD_9:24
.= <%((- b) * (- b)),((b * (1. R)) + ((1. R) * (- b))),(1. R)%> by C, t2
.= <%((- b) * (- b)),(0. R),(1. R)%> by RLVECT_1:5
.= <%(b * b),(0. R),(1. R)%> by VECTSP_1:10
.= <%(b |^ 2),(0. R),(1. R)%> by RING_5:3
.= <%(- a),(0. R),(1. R)%> by AS, C, t2 ;

now :: thesis: for j being Nat holds ((X- b) `^ p) . j = (X^ (p,a)) . j

let j be Nat; :: thesis: ((X- b) `^ p) . b₁ = (X^ (p,a)) . b₁
( j <= 2 implies not not j = 0 & ... & not j = 2 ) ;

per cases then ( j = 0 or j = 2 or j = 1 or j > 2 ) ;

suppose E: j = 0 ; :: thesis: ((X- b) `^ p) . b₁ = (X^ (p,a)) . b₁

hence ((X- b) `^ p) . j = - a by D, FIELD_9:16
.= (X^ (p,a)) . j by E, Lm10 ;
:: thesis: verum

end;

suppose E: j = 2 ; :: thesis: ((X- b) `^ p) . b₁ = (X^ (p,a)) . b₁

hence ((X- b) `^ p) . j = 1. R by D, FIELD_9:16
.= (X^ (p,a)) . j by E, C, Lm10 ;
:: thesis: verum

end;

suppose E: j = 1 ; :: thesis: ((X- b) `^ p) . b₁ = (X^ (p,a)) . b₁

hence ((X- b) `^ p) . j = 0. R by D, FIELD_9:16
.= (X^ (p,a)) . j by E, C, Lm11 ;
:: thesis: verum

end;

suppose E: j > 2 ; :: thesis: ((X- b) `^ p) . b₁ = (X^ (p,a)) . b₁

then j >= 2 + 1 by INT_1:7;
hence ((X- b) `^ p) . j = 0. R by D, FIELD_9:16
.= (X^ (p,a)) . j by E, C, Lm11 ;
:: thesis: verum

end;

end;

end;

hence X^ (p,a) = (X- b) `^ p
.= (X- b) |^ p ;
:: thesis: verum

end;

suppose H0: p <> 2 ; :: thesis: X^ (p,a) = (X- b) |^ p

( p <= 2 implies not not p = 0 & ... & not p = 2 ) ;
then H: p is 2 _greater by H0, INT_2:def 4, NAT_6:def 1;
set q = X^ (p,a);
reconsider q1 = <%(0. R),(1. R)%>, q2 = <%(- b)%> as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
set r = (q1 `^ p) + (q2 `^ p);
q2 = <%(- b),(0. R)%> by POLYNOM5:43;
then A: q1 + q2 = <%(0. R),(1. R)%> + <%(- b),(0. R)%> by POLYNOM3:def 10
.= <%((0. R) + (- b)),((1. R) + (0. R))%> by NIVEN:30
.= X- b by RING_5:10 ;
B: (q1 + q2) |^ p = (q1 |^ p) + (q2 |^ p) by fresh;

now :: thesis: for j being Nat holds (X^ (p,a)) . j = ((q1 `^ p) + (q2 `^ p)) . j

let j be Nat; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁
D0: ((q1 `^ p) + (q2 `^ p)) . j = ((q1 `^ p) . j) + ((q2 `^ p) . j) by NORMSP_1:def 2;
H1: j is Element of NAT by ORDINAL1:def 12;

per cases ( j in Support (X^ (p,a)) or not j in Support (X^ (p,a)) ) ;

suppose j in Support (X^ (p,a)) ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

then (X^ (p,a)) . j <> 0. R by POLYNOM1:def 3;

per cases then ( j = p or j = 0 ) by Lm11;

suppose D: j = p ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

then D4: j >= 1 by INT_2:def 4;
D1: (<%(- b)%> `^ p) . j = <%(power ((- b),p))%> . j by POLYNOM5:36
.= 0. R by H1, D4, POLYNOM5:32 ;
D5: q1 = rpoly (1,(- (0. R))) by RING_5:10;
D3: deg (<%(0. R),(1. R)%> `^ p) = p * (deg <%(0. R),(1. R)%>) by t1
.= p * 1 by D5, HURWITZ:27 ;
thus (X^ (p,a)) . j = 1. R by D, Lm10
.= (LC (<%(0. R),(1. R)%> `^ p)) + ((<%(- b)%> `^ p) . j) by D1, D5, RATFUNC1:def 7
.= ((q1 `^ p) + (q2 `^ p)) . j by D0, D3, D, FIELD_6:2 ; :: thesis: verum

end;

suppose D: j = 0 ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

then D1: (<%(0. R),(1. R)%> `^ p) . j = (<%(0. R),(1. R)%> . 0) |^ p by t3
.= (0. R) |^ p by POLYNOM5:38
.= 0. R ;
thus (X^ (p,a)) . j = - (b |^ p) by D, AS, Lm10
.= (- b) |^ p by H, todd
.= <%(power ((- b),p))%> . j by D, POLYNOM5:32
.= ((q1 `^ p) + (q2 `^ p)) . j by D0, D1, POLYNOM5:36 ; :: thesis: verum

end;

end;

end;

suppose D: not j in Support (X^ (p,a)) ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

then D8: (X^ (p,a)) . j = 0. R by H1, POLYNOM1:def 4;

per cases ( j = 0 or j = p or ( j <> 0 & j <> p ) ) ;

suppose D1: j = 0 ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

then D2: - a = 0. R by D8, Lm10;
D3: (<%(- b)%> `^ p) . 0 = (<%(- b)%> . 0) |^ p by t3
.= (- b) |^ p by POLYNOM5:32
.= 0. R by AS, D2, H, todd ;
(<%(0. R),(1. R)%> `^ p) . 0 = (<%(0. R),(1. R)%> . 0) |^ p by t3
.= (0. R) |^ p by POLYNOM5:38
.= 0. R ;
hence (X^ (p,a)) . j = ((q1 `^ p) + (q2 `^ p)) . j by D0, D, D1, D3, POLYNOM1:def 4; :: thesis: verum

end;

suppose j = p ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

hence (X^ (p,a)) . j = ((q1 `^ p) + (q2 `^ p)) . j by D8, Lm10; :: thesis: verum

end;

suppose D2: ( j <> 0 & j <> p ) ; :: thesis: (X^ (p,a)) . b₁ = ((q1 `^ p) + (q2 `^ p)) . b₁

then D4: j >= 1 + 0 by INT_1:7;
(<%(- b)%> `^ p) . j = <%(power ((- b),p))%> . j by POLYNOM5:36
.= 0. R by D4, H1, POLYNOM5:32 ;
hence (X^ (p,a)) . j = ((q1 `^ p) + (q2 `^ p)) . j by D8, D0, D2, t4; :: thesis: verum

end;

end;

end;

end;

end;

hence X^ (p,a) = (q1 `^ p) + (q2 `^ p)
.= (X- b) |^ p by B, A, POLYNOM3:def 10 ;
:: thesis: verum

end;

end;