theorem :: POLYNOM4:13
for L being non empty ZeroStr holds Leading-Monomial (0_. L) = 0_. L