let L be non degenerated Ring; :: thesis: for x being Element of L holds eval ((npoly (L,0)),x) = 1. L
let x be Element of L; :: thesis: eval ((npoly (L,0)),x) = 1. L
set q = npoly (L,0);
consider F being FinSequence of L such that
A3: eval ((npoly (L,0)),x) = Sum F and
A4: len F = len (npoly (L,0)) and
A5: for n being Element of NAT st n in dom F holds
F . n = ((npoly (L,0)) . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def 2;
0 = deg (npoly (L,0)) by lem6
.= (len (npoly (L,0))) - 1 by HURWITZ:def 2 ;
then C: F = <*(F . 1)*> by A4, FINSEQ_1:40;
then Seg 1 = dom F by FINSEQ_1:38;
then F . 1 = ((npoly (L,0)) . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A5, FINSEQ_1:3
.= ((npoly (L,0)) . 0) * ((power L) . (x,(1 -' 1))) by NAT_2:8
.= ((npoly (L,0)) . 0) * ((power L) . (x,0)) by NAT_2:8
.= (1. L) * ((power L) . (x,0)) by Lm10
.= (1. L) * (1_ L) by GROUP_1:def 7
.= 1. L ;
hence eval ((npoly (L,0)),x) = 1. L by A3, C, RLVECT_1:44; :: thesis: verum