:: deftheorem defines FinSeq2Matrix MATRIXC1:def 3 :
for x being FinSequence of COMPLEX st len x > 0 holds
for b₂ being Matrix of COMPLEX holds
( b₂ = FinSeq2Matrix x iff ( len b₂ = len x & width b₂ = 1 & ( for j being Nat st j in Seg (len x) holds
b₂ . j = <*(x . j)*> ) ) );