let i, m, n, k be Element of NAT ; :: thesis: 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) )
let G be Go-board; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m implies ( (DelCol G,i) * n,k = G * n,(k + 1) & k + 1 in Seg (width G) ) )
assume A1: ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m ) ; :: thesis: ( (DelCol G,i) * n,k = G * n,(k + 1) & k + 1 in Seg (width G) )
then A2: ( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) ) by Th30;
A3: ( dom G = Seg (len G) & Seg (len (DelCol G,i)) = dom (DelCol G,i) ) by FINSEQ_1:def 3;
1 < width G by A1, Th3;
then len (DelCol G,i) = len G by A1, Def10;
hence (DelCol G,i) * n,k = (Col G,(k + 1)) . n by A1, A2, A3, MATRIX_1:def 9
.= G * n,(k + 1) by A1, MATRIX_1:def 9 ;
:: thesis: k + 1 in Seg (width G)
thus k + 1 in Seg (width G) by A1, Th30; :: thesis: verum