let R be non degenerated Ring; :: thesis: for n being non trivial Nat
for a being Element of R holds eval ((X^ (n,R)),a) = (a |^ n) - a
let n be non trivial Nat; :: thesis: for a being Element of R holds eval ((X^ (n,R)),a) = (a |^ n) - a
let x be Element of R; :: thesis: eval ((X^ (n,R)),x) = (x |^ n) - x
set q = X^ (n,R);
consider F being FinSequence of R such that
A3: eval ((X^ (n,R)),x) = Sum F and
A4: len F = len (X^ (n,R)) and
A5: for j being Element of NAT st j in dom F holds
F . j = ((X^ (n,R)) . (j -' 1)) * ((power R) . (x,(j -' 1))) by POLYNOM4:def 2;
A: n = deg (X^ (n,R)) by Lm12
.= (len (X^ (n,R))) - 1 by HURWITZ:def 2 ;
then B: len (X^ (n,R)) = n + 1 ;
C: dom F = Seg (n + 1) by A, A4, FINSEQ_1:def 3;
D: 1 <= n + 1 by NAT_1:11;
E: (n + 1) -' 1 = (n + 1) - 1 by NAT_1:11, XREAL_1:233;
B1: F . (n + 1) = ((X^ (n,R)) . n) * ((power R) . (x,((n + 1) -' 1))) by E, A5, D, C, FINSEQ_1:1
.= (1. R) * ((power R) . (x,((n + 1) -' 1))) by Lm10
.= x |^ n by E ;

B2: now :: thesis: for j being Element of NAT st 1 <= j & j <= n & j <> 2 holds
F . j = 0. R

let j be Element of NAT ; :: thesis: ( 1 <= j & j <= n & j <> 2 implies F . b₁ = 0. R )
assume H0: ( 1 <= j & j <= n & j <> 2 ) ; :: thesis: F . b₁ = 0. R
reconsider j1 = j -' 1 as Element of NAT ;
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
n <= n + 1 by NAT_1:11;
then H1: j <= n + 1 by H0, XXREAL_0:2;
H4: j1 = j - 1 by H0, XREAL_1:233;

per cases ( j = 1 or j <> 1 ) ;

suppose j = 1 ; :: thesis: F . b₁ = 0. R

then j1 = 0 by NAT_2:8;
hence F . j = ((X^ (n,R)) . 0) * ((power R) . (x,(j -' 1))) by A5, H1, C, H0, FINSEQ_1:1
.= (0. R) * ((power R) . (x,(j -' 1))) by Lm11
.= 0. R ;
:: thesis: verum

end;

suppose j <> 1 ; :: thesis: F . b₁ = 0. R

j1 + 1 <= n1 + 1 by H4, H0;
then H3: ( j1 <> n & j1 <> 1 ) by H4, H0, NAT_1:13;
thus F . j = ((X^ (n,R)) . j1) * ((power R) . (x,(j -' 1))) by A5, H1, C, H0, FINSEQ_1:1
.= (0. R) * ((power R) . (x,(j -' 1))) by H3, Lm11
.= 0. R ; :: thesis: verum

end;

end;

end;

B4: len F > 2 by NAT_2:29, NAT_1:13, A4, B;
then 2 in Seg (len F) by FINSEQ_1:1;
then 2 in dom F by FINSEQ_1:def 3;
then B3: F . 2 = ((X^ (n,R)) . (2 -' 1)) * ((power R) . (x,(2 -' 1))) by A5
.= ((X^ (n,R)) . (2 - 1)) * ((power R) . (x,(2 -' 1))) by XREAL_0:def 2
.= ((X^ (n,R)) . 1) * ((power R) . (x,(2 - 1))) by XREAL_0:def 2
.= (- (1. R)) * ((power R) . (x,1)) by Lm10
.= - ((1. R) * ((power R) . (x,(1 + 0)))) by VECTSP_1:9
.= - (((power R) . (x,0)) * x) by GROUP_1:def 7
.= - ((1_ R) * x) by GROUP_1:def 7
.= - x ;
consider fp being sequence of the carrier of R such that
A6: Sum F = fp . (len F) and
A7: fp . 0 = 0. R and
A8: for j being Nat
for v being Element of R st j < len F & v = F . (j + 1) holds
fp . (j + 1) = (fp . j) + v by RLVECT_1:def 12;
defpred S₁[ Element of NAT ] means ( ( $1 = 0 & fp . $1 = 0. R ) or ( $1 = 1 & fp . $1 = 0. R ) or ( 1 < $1 & $1 < len F & fp . $1 = - x ) or ( $1 = len F & fp . $1 = (x |^ n) - x ) );
IA: S₁[ 0 ] by A7;

IS: now :: thesis: for j being Element of NAT st 0 <= j & j < len F & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len F & S₁[j] implies S₁[b₁ + 1] )
assume C1: ( 0 <= j & j < len F ) ; :: thesis: ( S₁[j] implies S₁[b₁ + 1] )
assume C2: S₁[j] ; :: thesis: S₁[b₁ + 1]
( j <= 1 implies not not j = 0 & ... & not j = 1 ) ;

per cases then ( ( j = 0 & j < (len F) - 1 ) or ( j = 0 & j >= (len F) - 1 ) or ( j = 1 & j < (len F) - 1 ) or ( j = 1 & j >= (len F) - 1 ) or ( 1 < j & j < (len F) - 1 ) or ( 1 < j & j >= (len F) - 1 ) ) ;

suppose D1: ( j = 0 & j < (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

then ( j + 1 = 1 & j + 1 <= n ) by INT_1:7;
then F . (j + 1) = 0. R by B2;
then fp . (j + 1) = (fp . 0) + (0. R) by D1, A8, C1
.= 0. R by A7 ;
hence S₁[j + 1] by D1; :: thesis: verum

end;

suppose ( j = 0 & j >= (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

hence S₁[j + 1] by A, A4; :: thesis: verum

end;

suppose D1: ( j = 1 & j < (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

then fp . (j + 1) = (fp . j) + (- x) by B3, A8, C1
.= - x by D1, C2 ;
hence S₁[j + 1] by D1, B4; :: thesis: verum

end;

suppose D1: ( j = 1 & j >= (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

(len F) - 1 > 2 - 1 by B4, XREAL_1:8;
hence S₁[j + 1] by D1; :: thesis: verum

end;

suppose D1: ( 1 < j & j < (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

then D3: j + 1 <= n by A, A4, INT_1:7;
( 1 <= j + 1 & j + 1 <= n & j + 1 <> 2 ) by D1, A, A4, NAT_1:13;
then F . (j + 1) = 0. R by B2;
then fp . (j + 1) = (- x) + (0. R) by C2, D1, C1, A8;
hence S₁[j + 1] by D1, D3, B, A4, XXREAL_0:2, NAT_1:16; :: thesis: verum

end;

suppose D1: ( 1 < j & j >= (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

j + 1 <= len F by INT_1:7, C1;
then D2: (j + 1) - 1 <= (len F) - 1 by XREAL_1:9;
then j = n by A4, A, D1, XXREAL_0:1;
then fp . (j + 1) = (fp . j) + (x |^ n) by B1, A8, C1;
hence S₁[j + 1] by A4, A, B1, C2, D2, D1, XXREAL_0:1; :: thesis: verum

end;

end;

end;

I: for j being Element of NAT st 0 <= j & j <= len F holds
S₁[j] from INT_1:sch 7(IA, IS);
( len F > 1 + 1 & 1 + 1 > 1 + 0 ) by B4;
hence eval ((X^ (n,R)),x) = (x |^ n) - x by A6, A3, I; :: thesis: verum