:: deftheorem Def3 defines mConv POLYNOM8:def 4 :
for m being Nat
for L being non empty ZeroStr
for p being AlgSequence of L
for b₄ being Matrix of m,1,L holds
( b₄ = mConv (p,m) iff for i being Nat st 1 <= i & i <= m holds
b₄ * (i,1) = p . (i - 1) );