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 that
A1: ( i in Seg (width G) & width G > 1 & n in dom G ) and
A2: m in Seg (width (DelCol G,i)) ; :: thesis: (DelCol G,i) * n,m = (Del (Line G,n),i) . m
thus (DelCol G,i) * n,m = (Line (DelCol G,i),n) . m by A2, MATRIX_1:def 8
.= (Del (Line G,n),i) . m by A1, Th25 ; :: thesis: verum