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 7
.= (Del ((Line (G,n)),i)) . m by A1, Th25 ; :: thesis: verum