let D be non empty set ; 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; 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; ( 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)
; (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
; verum