theorem Th18: :: NIVEN:20

for n being Nat
for L being non empty ZeroStr
for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
len p = n + 1