:: deftheorem Def4 defines InterchangeCol MATRIX12:def 4 :
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 st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds
for b₇ being Matrix of n,m,K holds
( b₇ = InterchangeCol (M,l,k) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₇ * (i,j) = M * (i,k) ) & ( j = k implies b₇ * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b₇ * (i,j) = M * (i,j) ) ) ) ) );