let L be non empty ZeroStr ; :: thesis: Leading-Monomial (0_. L) = 0_. L
len (0_. L) = 0 by Th3;
hence Leading-Monomial (0_. L) = 0_. L by Th12; :: thesis: verum