for k, l, n, m being Nat
for K being Field
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