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

let i, j be Nat; :: thesis:
assume A3: [i,j] in Indices A ; :: thesis:
Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A4: i in Seg n by A3, ZFMISC_1:87;
then A5: 1 <= i by FINSEQ_1:1;
A6: ( i = i0 & j = i0 implies (SwapDiagonal (K,n,i0)) * (i,j) = 0. K ) by A1, Th43;
width A = n by MATRIX_0:24;
then A7: j in Seg n by A3, ZFMISC_1:87;
then A8: 1 <= j by FINSEQ_1:1;
A9: i <= n by A4, FINSEQ_1:1;
then A10: ( i = i0 & j = i0 implies A * (i,j) = 0. K ) by A2, A5;
A11: j <= n by A7, FINSEQ_1:1;
then A12: ( i = 1 & j = i0 implies A * (i,j) = 1. K ) by A2, A9, A8;
A13: ( i = 1 & j = 1 implies (SwapDiagonal (K,n,i0)) * (i,j) = 0. K ) by A1, A9, Th43;
A14: ( i = 1 & j = 1 implies A * (i,j) = 0. K ) by A2, A9;
A15: ( i = i0 & j = 1 implies A * (i,j) = 1. K ) by A2, A5, A9, A11;
( ( ( 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 A2, A5, A9, A8, A11;
hence A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j) by A1, A5, A9, A8, A11, A12, A15, A14, A10, A13, A6, Th43; :: thesis:

end;