let K be Field; :: thesis: for n, i0 being Element of NAT
for A being Matrix of n,K st 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n 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 ) ) ) ) ) holds
A = SwapDiagonal K,n,i0
let n, i0 be Element of NAT ; :: thesis: for A being Matrix of n,K st 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n 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 ) ) ) ) ) holds
A = SwapDiagonal K,n,i0
let A be Matrix of n,K; :: thesis: ( 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n 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 ) ) ) ) ) implies A = SwapDiagonal K,n,i0 )
assume A0: ( 1 <= i0 & i0 <= n & i0 <> 1 ) ; :: thesis: ( ex i, j being Nat st
( 1 <= i & i <= n & 1 <= j & j <= n & not ( ( 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 ) ) ) ) ) or A = SwapDiagonal K,n,i0 )
assume B0: for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n 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 ) ) ) ) ; :: 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 C0: [i,j] in Indices A ; :: thesis: A * i,j = (SwapDiagonal K,n,i0) * i,j
( len A = n & width A = n & Indices A = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
then ( i in Seg n & j in Seg n ) by C0, ZFMISC_1:106;
then B1: ( 1 <= i & i <= n & 1 <= j & j <= n ) by FINSEQ_1:3;
then B2: ( ( 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 ) ) ) ) by B0;
( ( i = 1 & j = i0 implies (SwapDiagonal K,n,i0) * i,j = 1. K ) & ( i = i0 & j = 1 implies (SwapDiagonal K,n,i0) * i,j = 1. K ) & ( i = 1 & j = 1 implies (SwapDiagonal K,n,i0) * i,j = 0. K ) & ( i = i0 & j = i0 implies (SwapDiagonal K,n,i0) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies (SwapDiagonal K,n,i0) * i,j = 1. K ) & ( i <> j implies (SwapDiagonal K,n,i0) * i,j = 0. K ) ) ) ) by XA, A0, B1;
hence A * i,j = (SwapDiagonal K,n,i0) * i,j by B2; :: thesis: verum

end;

hence A = SwapDiagonal K,n,i0 by MATRIX_1:28; :: thesis: verum