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)) @ = SwapDiagonal (K,n,i0)