:: deftheorem Def4 defines * POLYNOM5:def 4 :
for L being non empty multMagma
for p being sequence of L
for v being Element of L
for b₄ being sequence of L holds
( b₄ = v * p iff for n being Element of NAT holds b₄ . n = v * (p . n) );