theorem :: MATRIX_0:61
for D being non empty set
for M being Matrix of D
for i being Nat st not i in Seg (width M) holds
DelCol (M,i) = M