let K be Field; :: thesis: 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)
let n, i0 be Element of NAT ; :: thesis: 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)
let A be Matrix of n,K; :: thesis: ( 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 ) ) ) implies A = SwapDiagonal (K,n,i0) )
assume A1: i0 = 1 ; :: thesis: ( ex i, j being Nat st
( 1 <= i & i <= n & 1 <= j & j <= n & not ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) or A = SwapDiagonal (K,n,i0) )
assume A2: 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 ) ) ; :: thesis: A = SwapDiagonal (K,n,i0)
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j) )
assume A3: [i,j] in Indices A ; :: thesis: A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j)
Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
then i in Seg n by A3, ZFMISC_1:87;
then A4: ( 1 <= i & i <= n ) by FINSEQ_1:1;
then A5: ( i = j implies A * (i,j) = 1. K ) by A2;
width A = n by MATRIX_0:24;
then j in Seg n by A3, ZFMISC_1:87;
then A6: ( 1 <= j & j <= n ) by FINSEQ_1:1;
then ( i <> j implies A * (i,j) = 0. K ) by A2, A4;
hence A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j) by A1, A4, A6, A5, Th44, Th45; :: thesis: verum

end;

hence A = SwapDiagonal (K,n,i0) by MATRIX_0:27; :: thesis: verum