:: deftheorem Def1 defines Leading-Monomial POLYNOM4:def 1 :
for L being non empty ZeroStr
for p being Polynomial of L
for b₃ being sequence of L holds
( b₃ = Leading-Monomial p iff ( b₃ . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
b₃ . n = 0. L ) ) );