let D be non empty set ; :: thesis: for M being Matrix of D
for i, j being Element of NAT st j in dom M & i in Seg (width M) holds
(Col M,i) . j = (Line M,j) . i
let M be Matrix of D; :: thesis: for i, j being Element of NAT st j in dom M & i in Seg (width M) holds
(Col M,i) . j = (Line M,j) . i
let i, j be Element of NAT ; :: thesis: ( j in dom M & i in Seg (width M) implies (Col M,i) . j = (Line M,j) . i )
assume that
A1: j in dom M and
A2: i in Seg (width M) ; :: thesis: (Col M,i) . j = (Line M,j) . i
thus (Col M,i) . j = M * j,i by A1, MATRIX_1:def 9
.= (Line M,j) . i by A2, MATRIX_1:def 8 ; :: thesis: verum