let D be non empty set ; :: thesis: for M being Matrix of D
for i, j being 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 Nat st j in dom M & i in Seg (width M) holds
(Col (M,i)) . j = (Line (M,j)) . i
let i, j be 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, Def8
.= (Line (M,j)) . i by A2, Def7 ; :: thesis: verum