theorem Th16: :: MATRIX12:16

for l, n, m being Nat
for K being comRing
for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(SXLine (M1,l,a)) @ = SXCol (M,l,a)