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 that
A1: i in Seg (width G) and
A2: ( width G = m + 1 & m > 0 ) and
A3: n in dom G and
A4: ( i <= k & k <= m ) ; :: thesis: ( (DelCol G,i) * n,k = G * n,(k + 1) & k + 1 in Seg (width G) )
1 < width G by A2, Th3;
then A5: len (DelCol G,i) = len G by A1, Def10;
A6: ( dom G = Seg (len G) & Seg (len (DelCol G,i)) = dom (DelCol G,i) ) by FINSEQ_1:def 3;
Col (DelCol G,i),k = Col G,(k + 1) by A1, A2, A4, Th30;
hence (DelCol G,i) * n,k = (Col G,(k + 1)) . n by A3, A6, A5, MATRIX_1:def 9
.= G * n,(k + 1) by A3, MATRIX_1:def 9 ;
:: thesis: k + 1 in Seg (width G)
thus k + 1 in Seg (width G) by A1, A2, A4, Th30; :: thesis: verum