theorem Th16: :: UPROOTS:19

for L being non empty ZeroStr
for p being AlgSequence of L st len p = 1 holds
( p = <%(p . 0)%> & p . 0 <> 0. L )