for n being Element of NAT
for K being Field
for i0 being Element of NAT st 1 <= i0 & i0 <= n holds
( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) )