:: deftheorem Def8 defines Col MATRIX_0:def 8 :
for D being non empty set
for M being Matrix of D
for i being Nat
for b₄ being FinSequence of D holds
( b₄ = Col (M,i) iff ( len b₄ = len M & ( for j being Nat st j in dom M holds
b₄ . j = M * (j,i) ) ) );