theorem Th11: :: MATRIX12:11

for k, l, n, m being Nat
for K being comRing
for M being Matrix of n,m,K st l in dom M & k in dom M holds
ILine ((ILine (M,l,k)),l,k) = M