:: deftheorem Def4 defines aConv POLYNOM8:def 5 :
for L being non empty ZeroStr
for M being Matrix of L
for b₃ being AlgSequence of L holds
( b₃ = aConv M iff ( ( for i being Nat st i < len M holds
b₃ . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b₃ . i = 0. L ) ) );