let i, m, k be Element of NAT ; :: thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) )
let G be Go-board; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m implies ( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) ) )
set N = DelCol G,i;
assume A1: ( i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m ) ; :: thesis: ( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) )
then A2: ( 1 <= i & i <= m + 1 & width (DelCol G,i) = m ) by Th26, FINSEQ_1:3;
then A3: ( 1 <= k + 1 & k + 1 <= m + 1 & 1 <= k ) by A1, NAT_1:11, XREAL_1:8, XXREAL_0:2;
then A4: ( k + 1 in Seg (width G) & k in Seg (width (DelCol G,i)) ) by A1, A2, FINSEQ_1:3;
A5: ( len (Col (DelCol G,i),k) = len (DelCol G,i) & len (Col G,(k + 1)) = len G ) by MATRIX_1:def 9;
A6: 1 < width G by A1, Th3;
then A7: len (DelCol G,i) = len G by A1, Def10;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col (DelCol G,i),k) implies (Col (DelCol G,i),k) . j = (Col G,(k + 1)) . j )
assume ( 1 <= j & j <= len (Col (DelCol G,i),k) ) ; :: thesis: (Col (DelCol G,i),k) . j = (Col G,(k + 1)) . j
then A8: j in dom (DelCol G,i) by A5, FINSEQ_3:27;
A9: ( dom (DelCol G,i) = Seg (len (DelCol G,i)) & dom G = Seg (len G) ) by FINSEQ_1:def 3;
A10: len (Line G,j) = m + 1 by A1, MATRIX_1:def 8;
A11: dom (Line G,j) = Seg (len (Line G,j)) by FINSEQ_1:def 3;
thus (Col (DelCol G,i),k) . j = (DelCol G,i) * j,k by A8, MATRIX_1:def 9
.= (Del (Line G,j),i) . k by A1, A4, A6, A7, A8, A9, Th28
.= (Line G,j) . (k + 1) by A1, A10, A11, FINSEQ_3:120
.= (Col G,(k + 1)) . j by A4, A7, A8, A9, Th17 ; :: thesis: verum

end;

hence ( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) ) by A1, A2, A3, A5, A7, FINSEQ_1:3, FINSEQ_1:18; :: thesis: verum