:: deftheorem defines Matrix2FinSeq MATRIXC1:def 4 :
for M being Matrix of COMPLEX holds Matrix2FinSeq M = Col (M,1);