theorem Th40: :: POLYNOM5:40

for L being non empty ZeroStr
for z0, z1 being Element of L st z1 <> 0. L holds
len <%z0,z1%> = 2