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

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