let i, m, n, k be Element of NAT ; :: thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
let G be Go-board; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i implies ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) ) )
assume that
A1: i in Seg (width G) and
A2: ( width G = m + 1 & m > 0 ) and
A3: n in dom G and
A4: ( 1 <= k & k < i ) ; :: thesis: ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
1 < width G by A2, SEQM_3:43;
then A5: len (DelCol (G,i)) = len G by A1, Def10;
A6: ( dom G = Seg (len G) & Seg (len (DelCol (G,i))) = dom (DelCol (G,i)) ) by FINSEQ_1:def 3;
Col ((DelCol (G,i)),k) = Col (G,k) by A1, A2, A4, Th29;
hence (DelCol (G,i)) * (n,k) = (Col (G,k)) . n by A3, A6, A5, MATRIX_1:def 8
.= G * (n,k) by A3, MATRIX_1:def 8 ;
:: thesis: k in Seg (width G)
thus k in Seg (width G) by A1, A2, A4, Th29; :: thesis: verum