:: deftheorem Def1 defines * POLYNOM1:def 1 :
for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b₄ being FinSequence of the carrier of L holds
( b₄ = a * p iff ( dom b₄ = dom p & ( for i being object st i in dom p holds
b₄ /. i = a * (p /. i) ) ) );