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:29;
(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:16; :: thesis: verum