theorem Th43: :: MATRIX14:43

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