let i, k be Element of NAT ; :: thesis: for G being Go-board st i in Seg (width G) & width G > 1 & k in dom G holds
Line (DelCol G,i),k = Del (Line G,k),i
let G be Go-board; :: thesis: ( i in Seg (width G) & width G > 1 & k in dom G implies Line (DelCol G,i),k = Del (Line G,k),i )
set D = DelCol G,i;
assume that
A1: ( i in Seg (width G) & width G > 1 ) and
A2: k in dom G ; :: thesis: Line (DelCol G,i),k = Del (Line G,k),i
len (DelCol G,i) = len G by A1, Def10;
then A3: dom (DelCol G,i) = dom G by FINSEQ_3:31;
(DelCol G,i) . k = Del (Line G,k),i by A1, A2, Def10;
hence Line (DelCol G,i),k = Del (Line G,k),i by A2, A3, MATRIX_2:18; :: thesis: verum