:: deftheorem defines ColVec2Mx MATRIX15:def 2 :
for D being non empty set
for b being FinSequence of D holds ColVec2Mx b = <*b*> @ ;