theorem Th68: :: MATRIX_0:68

for D being non empty set
for G being Matrix of D
for i, k, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )