:: deftheorem Def11 defines NormPolynomial POLYNOM5:def 11 :
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for p being Polynomial of L
for b₃ being sequence of L holds
( b₃ = NormPolynomial p iff for n being Element of NAT holds b₃ . n = (p . n) / (p . ((len p) -' 1)) );