theorem Th70: :: MATRIX_0:70

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