let i, n, m be Element of NAT ; :: thesis: for G being Go-board st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol G,i)) holds
(DelCol G,i) * n,m = (Del (Line G,n),i) . m
let G be Go-board; :: thesis: ( i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol G,i)) implies (DelCol G,i) * n,m = (Del (Line G,n),i) . m )
assume A1: ( i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol G,i)) ) ; :: thesis: (DelCol G,i) * n,m = (Del (Line G,n),i) . m
hence (DelCol G,i) * n,m = (Line (DelCol G,i),n) . m by MATRIX_1:def 8
.= (Del (Line G,n),i) . m by A1, Th25 ;
:: thesis: verum