theorem Th14: :: UPROOTS:17

for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff len p > 0 )