for D being non empty set
for bD being FinSequence of D
for MD being Matrix of D st ( len MD <> 0 or len bD <> 0 ) holds
( MD = ColVec2Mx bD iff ( Col (MD,1) = bD & width MD = 1 ) )