let m, k, n be Element of NAT ; :: thesis: for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( k in Seg (width G) & (DelCol G,(width G)) * n,k = G * n,k & width G in Seg (width G) )
let G be Go-board; :: thesis: ( width G = m + 1 & m > 0 & k in Seg m & n in dom G implies ( k in Seg (width G) & (DelCol G,(width G)) * n,k = G * n,k & width G in Seg (width G) ) )
assume A1: ( width G = m + 1 & m > 0 & k in Seg m & n in dom G ) ; :: thesis: ( k in Seg (width G) & (DelCol G,(width G)) * n,k = G * n,k & width G in Seg (width G) )
then 1 <= width G by Th3;
then A2: ( width G in Seg (width G) & 1 <= k & k <= m & m < m + 1 ) by A1, FINSEQ_1:3, NAT_1:13;
then k < width G by A1, XXREAL_0:2;
hence ( k in Seg (width G) & (DelCol G,(width G)) * n,k = G * n,k & width G in Seg (width G) ) by A1, A2, Th31; :: thesis: verum