theorem Th42: :: MATRIX_0:42

for D being 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