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 that
A1: i in Seg (width G) and
A2: width G = m + 1 and
A3: m > 0 and
A4: 1 <= k and
A5: k < i ; :: thesis: ( Col (DelCol G,i),k = Col G,k & k in Seg (width (DelCol G,i)) & k in Seg (width G) )
A6: width (DelCol G,i) = m by A1, A2, A3, Th26;
A7: 1 < width G by A2, A3, Th3;
then A8: len (DelCol G,i) = len G by A1, Def10;
i <= m + 1 by A1, A2, FINSEQ_1:3;
then A9: k < m + 1 by A5, XXREAL_0:2;
then A10: k in Seg (width G) by A2, A4, FINSEQ_1:3;
A11: len (Col G,k) = len G by MATRIX_1:def 9;
A12: len (Col (DelCol G,i),k) = len (DelCol G,i) by MATRIX_1:def 9;
A13: k <= m by A9, NAT_1:13;
then A14: k in Seg (width (DelCol G,i)) by A4, A6, FINSEQ_1:3;

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 )
A15: ( dom (DelCol G,i) = Seg (len (DelCol G,i)) & dom G = Seg (len G) ) by FINSEQ_1:def 3;
A16: len (Line G,j) = m + 1 by A2, MATRIX_1:def 8;
assume ( 1 <= j & j <= len (Col (DelCol G,i),k) ) ; :: thesis: (Col (DelCol G,i),k) . j = (Col G,k) . j
then A17: j in dom (DelCol G,i) by A12, FINSEQ_3:27;
hence (Col (DelCol G,i),k) . j = (DelCol G,i) * j,k by MATRIX_1:def 9
.= (Del (Line G,j),i) . k by A1, A14, A7, A8, A17, A15, Th28
.= (Line G,j) . k by A5, A16, FINSEQ_3:119
.= (Col G,k) . j by A10, A8, A17, A15, 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 A2, A4, A6, A9, A13, A12, A11, A8, FINSEQ_1:3, FINSEQ_1:18; :: thesis: verum