theorem lem1a: :: RING_5:46
for R being non degenerated Ring
for n being non zero Nat
for x being Element of R holds eval ((npoly (R,n)),x) = (x |^ n) + (1. R)