:: deftheorem defines SwapDiagonal MATRIX14:def 3 :
for K being Field
for n being Element of NAT
for i0 being Nat holds SwapDiagonal (K,n,i0) = Swap ((1. (K,n)),1,i0);