theorem Th15: :: POLYNOM4:15

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