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 that
A1: width G = m + 1 and
A2: m > 0 and
A3: 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) )
1 <= width G by A1, A2, SEQM_3:43;
then A4: 1 in Seg (width G) by FINSEQ_1:1;
( 1 <= k & k <= m ) by A3, FINSEQ_1:1;
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, A4, Th30; :: thesis: verum