theorem Th29: :: POLYNOM8:29

for m being Nat st m > 0 holds
for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M