let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K
for j0 being Element of NAT st 1 <= j0 & j0 <= n holds
( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j ) )
let K be Field; :: thesis: for A being Matrix of n,K
for j0 being Element of NAT st 1 <= j0 & j0 <= n holds
( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j ) )
let A be Matrix of n,K; :: thesis: for j0 being Element of NAT st 1 <= j0 & j0 <= n holds
( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j ) )
let j0 be Element of NAT ; :: thesis: ( 1 <= j0 & j0 <= n implies ( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j ) ) )
assume A1: ( 1 <= j0 & j0 <= n ) ; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j ) )
A5: ((SwapDiagonal K,n,j0) * (A @ )) @ = ((A @ ) @ ) * ((SwapDiagonal K,n,j0) @ ) by AA44
.= A * ((SwapDiagonal K,n,j0) @ ) by MATRIXR2:29
.= A * (SwapDiagonal K,n,j0) by AA4160, A1 ;
A12: for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies ( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) )
assume B1: ( 1 <= i & i <= n ) ; :: thesis: ( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 )
then X: 1 <= n by XXREAL_0:2;
B2: [j0,i] in Indices ((SwapDiagonal K,n,j0) * (A @ )) by B1, A1, MATRIX_1:38;
B15: [1,i] in Indices ((SwapDiagonal K,n,j0) * (A @ )) by B1, X, MATRIX_1:38;
B3: [i,1] in Indices A by B1, X, MATRIX_1:38;
B14: [i,j0] in Indices A by B1, A1, MATRIX_1:38;
thus (A * (SwapDiagonal K,n,j0)) * i,j0 = ((SwapDiagonal K,n,j0) * (A @ )) * j0,i by B2, A5, MATRIX_1:def 7
.= (A @ ) * 1,i by B1, A1, AA4100
.= A * i,1 by B3, MATRIX_1:def 7 ; :: thesis: (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0
thus (A * (SwapDiagonal K,n,j0)) * i,1 = ((SwapDiagonal K,n,j0) * (A @ )) * 1,i by B15, A5, MATRIX_1:def 7
.= (A @ ) * j0,i by B1, A1, AA4100
.= A * i,j0 by B14, MATRIX_1:def 7 ; :: thesis: verum

end;

for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j

proof

let i, j be Element of NAT ; :: thesis: ( j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n implies (A * (SwapDiagonal K,n,j0)) * i,j = A * i,j )
assume B1: ( j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: (A * (SwapDiagonal K,n,j0)) * i,j = A * i,j
B15: [j,i] in Indices ((SwapDiagonal K,n,j0) * (A @ )) by B1, MATRIX_1:38;
B17: [i,j] in Indices A by B1, MATRIX_1:38;
thus (A * (SwapDiagonal K,n,j0)) * i,j = ((SwapDiagonal K,n,j0) * (A @ )) * j,i by B15, A5, MATRIX_1:def 7
.= (A @ ) * j,i by B1, A1, AA4100
.= A * i,j by B17, MATRIX_1:def 7 ; :: thesis: verum

end;

hence ( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal K,n,j0)) * i,j0 = A * i,1 & (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0 ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal K,n,j0)) * i,j = A * i,j ) ) by A12; :: thesis: verum