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 & 1 <= k & k < i holds
( Col (DelCol G,i),k = Col G,k & k in Seg (width (DelCol G,i)) & k in Seg (width G) )
let G be Go-board; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i implies ( Col (DelCol G,i),k = Col G,k & k in Seg (width (DelCol G,i)) & k in Seg (width G) ) )
set N = DelCol G,i;
assume A1: ( i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i ) ; :: thesis: ( Col (DelCol G,i),k = Col G,k & k in Seg (width (DelCol G,i)) & k in Seg (width G) )
then A2: ( 1 <= i & i <= m + 1 & width (DelCol G,i) = m ) by Th26, FINSEQ_1:3;
then k < m + 1 by A1, XXREAL_0:2;
then A3: ( k <= m + 1 & k <= m ) by NAT_1:13;
then A4: ( k 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) = 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) . j )
assume ( 1 <= j & j <= len (Col (DelCol G,i),k) ) ; :: thesis: (Col (DelCol G,i),k) . j = (Col G,k) . 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;
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 by A1, A10, FINSEQ_3:119
.= (Col G,k) . j by A4, A7, A8, A9, Th17 ; :: thesis: verum

end;

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