theorem :: MATRIX_0:74

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