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