let i, m be Element of NAT ; :: thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 holds
width (DelCol (G,i)) = m
let G be Go-board; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 implies width (DelCol (G,i)) = m )
set D = DelCol (G,i);
assume that
A1: i in Seg (width G) and
A2: width G = m + 1 and
A3: m > 0 ; :: thesis: width (DelCol (G,i)) = m
0 < len G by Lm1;
then 0 + 1 <= len G by NAT_1:13;
then A4: 1 in dom G by FINSEQ_3:27;
0 + 1 < width G by A2, A3, XREAL_1:8;
then A5: Line ((DelCol (G,i)),1) = Del ((Line (G,1)),i) by A1, A4, Th25;
A6: ( dom (Line (G,1)) = Seg (len (Line (G,1))) & len (Line ((DelCol (G,i)),1)) = width (DelCol (G,i)) ) by FINSEQ_1:def 3, MATRIX_1:def 8;
len (Line (G,1)) = m + 1 by A2, MATRIX_1:def 8;
hence width (DelCol (G,i)) = m by A1, A2, A5, A6, FINSEQ_3:118; :: thesis: verum