for K being Field
for n being Element of NAT
for A being Matrix of n,K
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds
(SwapDiagonal (K,n,1)) * (i,j) = 0. K