:: deftheorem Def1 defines InterchangeLine MATRIX12:def 1 :
for n, m being Nat
for K being non empty 1-sorted
for M being Matrix of n,m,K
for l, k being Nat
for b₇ being Matrix of n,m,K holds
( b₇ = InterchangeLine (M,l,k) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₇ * (i,j) = M * (k,j) ) & ( i = k implies b₇ * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b₇ * (i,j) = M * (i,j) ) ) ) ) );