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 A1: ( j in dom M & i in Seg (width M) ) ; :: thesis: (Col M,i) . j = (Line M,j) . i
hence (Col M,i) . j = M * j,i by MATRIX_1:def 9
.= (Line M,j) . i by A1, MATRIX_1:def 8 ;
:: thesis: verum