theorem Th41: :: POLYNOM5:41

for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0,(0. L)%> = 1