theorem Th15: :: MATRIX12:15

for k, l, n, m being Nat
for K being comRing
for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(ILine (M1,l,k)) @ = ICol (M,l,k)