:: deftheorem Def13 defines DelCol MATRIX_0:def 13 :
for i being Nat
for D being non empty set
for M, b₄ being Matrix of D holds
( b₄ = DelCol (M,i) iff ( len b₄ = len M & ( for k being Nat st k in dom M holds
b₄ . k = Del ((Line (M,k)),i) ) ) );