:: deftheorem Def9 defines ColVec2Mx MATRIXR1:def 9 :
for x being FinSequence of REAL st len x > 0 holds
for b₂ being Matrix of REAL holds
( b₂ = ColVec2Mx x iff ( len b₂ = len x & width b₂ = 1 & ( for j being Nat st j in dom x holds
b₂ . j = <*(x . j)*> ) ) );