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 8
.= (Line (M,j)) . i by A2, MATRIX_1:def 7 ; :: thesis: verum