theorem Th64: :: MATRIX_0:64

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