theorem Th28: :: POLYNOM8:28

for m being Nat st m > 0 holds
for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )