:: deftheorem Def5 defines monomial HILBASIS:def 5 :
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Nat
for a being Element of L
for b₄ being Polynomial of L holds
( b₄ = monomial (a,n) iff for x being Nat holds
( ( x = n implies b₄ . x = a ) & ( x <> n implies b₄ . x = 0. L ) ) );