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;
A1: dom (Line G,1) = Seg (len (Line G,1)) by FINSEQ_1:def 3;
assume A2: ( i in Seg (width G) & width G = m + 1 & m > 0 ) ; :: thesis: width (DelCol G,i) = m
then A3: ( 0 + 1 < width G & 0 < len G ) by Lm1, XREAL_1:8;
then 0 + 1 <= len G by NAT_1:13;
then 1 in dom G by FINSEQ_3:27;
then ( Line (DelCol G,i),1 = Del (Line G,1),i & len (Line G,1) = m + 1 & len (Line (DelCol G,i),1) = width (DelCol G,i) ) by A2, A3, Th25, MATRIX_1:def 8;
hence width (DelCol G,i) = m by A1, A2, FINSEQ_3:118; :: thesis: verum