:: deftheorem defines degree HURWITZ:def 2 :
for L being non empty ZeroStr
for p being Polynomial of L holds degree p = (len p) - 1;