let m, k be Element of NAT ; :: thesis: for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col (DelCol G,1),k = Col G,(k + 1) & k in Seg (width (DelCol G,1)) & k + 1 in Seg (width G) )
let G be Go-board; :: thesis: ( width G = m + 1 & m > 0 & k in Seg m implies ( Col (DelCol G,1),k = Col G,(k + 1) & k in Seg (width (DelCol G,1)) & k + 1 in Seg (width G) ) )
assume A1: ( width G = m + 1 & m > 0 & k in Seg m ) ; :: thesis: ( Col (DelCol G,1),k = Col G,(k + 1) & k in Seg (width (DelCol G,1)) & k + 1 in Seg (width G) )
then 1 <= width G by Th3;
then ( 1 in Seg (width G) & 1 <= k & k <= m ) by A1, FINSEQ_1:3;
hence ( Col (DelCol G,1),k = Col G,(k + 1) & k in Seg (width (DelCol G,1)) & k + 1 in Seg (width G) ) by A1, Th30; :: thesis: verum