theorem Th46: :: MATRIX14:46

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