let L be non degenerated Ring; for x being Element of L holds eval ((npoly (L,0)),x) = 1. L
let x be Element of L; 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; verum