for L being non empty ZeroStr
for p being Polynomial of L holds len (Leading-Monomial p) = len p