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