let R be non degenerated Ring; :: thesis: for n being non zero Nat
for a, x being Element of R holds eval ((anpoly (a,n)),x) = a * (x |^ n)
let n be non zero Nat; :: thesis: for a, x being Element of R holds eval ((anpoly (a,n)),x) = a * (x |^ n)
let a, x be Element of R; :: thesis: eval ((anpoly (a,n)),x) = a * (x |^ n)
set q = anpoly (a,n);

per cases ( a = 0. R or a <> 0. R ) ;

suppose A1: a = 0. R ; :: thesis: eval ((anpoly (a,n)),x) = a * (x |^ n)

then anpoly (a,n) = 0_. R by UPROOTS:def 5;
hence eval ((anpoly (a,n)),x) = a * (x |^ n) by A1, POLYNOM4:17; :: thesis: verum

end;

suppose a <> 0. R ; :: thesis: eval ((anpoly (a,n)),x) = a * (x |^ n)

then A2: not a is zero ;
consider F being FinSequence of R such that
A3: eval ((anpoly (a,n)),x) = Sum F and
A4: len F = len (anpoly (a,n)) and
A5: for j being Element of NAT st j in dom F holds
F . j = ((anpoly (a,n)) . (j -' 1)) * ((power R) . (x,(j -' 1))) by POLYNOM4:def 2;
n = deg (anpoly (a,n)) by A2, Lm1
.= (len (anpoly (a,n))) - 1 ;
then A7: dom F = Seg (n + 1) by A4, FINSEQ_1:def 3;
A8: 1 <= n + 1 by NAT_1:11;
A9: (n + 1) -' 1 = (n + 1) - 1 by NAT_1:11, XREAL_1:233;
A10: F /. (n + 1) = F . (n + 1) by A7, FINSEQ_1:3, PARTFUN1:def 6
.= ((anpoly (a,n)) . n) * ((power R) . (x,((n + 1) -' 1))) by A9, A5, A8, A7, FINSEQ_1:1
.= a * ((power R) . (x,((n + 1) -' 1))) by POLYDIFF:24
.= a * (x |^ n) by A9, BINOM:def 2 ;

now :: thesis: for j being Element of NAT st j in dom F & j <> n + 1 holds
F /. j = 0. R

let j be Element of NAT ; :: thesis: ( j in dom F & j <> n + 1 implies F /. j = 0. R )
assume A11: ( j in dom F & j <> n + 1 ) ; :: thesis: F /. j = 0. R
then A12: ( 1 <= j & j <= n + 1 ) by A7, FINSEQ_1:1;
then j < n + 1 by A11, XXREAL_0:1;
then A13: ( 1 <= j & j <= n ) by A11, NAT_1:13, A7, FINSEQ_1:1;
A14: j -' 1 = j - 1 by A12, XREAL_0:def 2;
A15: j - 1 < j - 0 by XREAL_1:15;
thus F /. j = F . j by A11, PARTFUN1:def 6
.= ((anpoly (a,n)) . (j -' 1)) * ((power R) . (x,(j -' 1))) by A5, A11
.= (0. R) * ((power R) . (x,(j -' 1))) by A15, A13, A14, POLYDIFF:25
.= 0. R ; :: thesis: verum

end;

hence eval ((anpoly (a,n)),x) = a * (x |^ n) by A3, A10, A7, FINSEQ_1:3, POLYNOM2:3; :: thesis: verum

end;

end;