theorem Th9: :: GOBOARD1:16

for n, m, i, k being Nat
for G being Go-board 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) ) by MATRIX_0:70;