theorem :: MATRIXR1:45

for x being FinSequence of REAL
for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )