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 ) )
A2: ((SwapDiagonal K,n,j0) * (A @ )) @ = ((A @ ) @ ) * ((SwapDiagonal K,n,j0) @ ) by Th30
.= A * ((SwapDiagonal K,n,j0) @ ) by MATRIXR2:29
.= A * (SwapDiagonal K,n,j0) by A1, Th50 ;
A3: 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 A4: ( 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 A5: 1 <= n by XXREAL_0:2;
then A6: [i,1] in Indices A by A4, MATRIX_1:38;
[j0,i] in Indices ((SwapDiagonal K,n,j0) * (A @ )) by A1, A4, MATRIX_1:38;
hence (A * (SwapDiagonal K,n,j0)) * i,j0 = ((SwapDiagonal K,n,j0) * (A @ )) * j0,i by A2, MATRIX_1:def 7
.= (A @ ) * 1,i by A1, A4, Th48
.= A * i,1 by A6, MATRIX_1:def 7 ;
:: thesis: (A * (SwapDiagonal K,n,j0)) * i,1 = A * i,j0
A7: [i,j0] in Indices A by A1, A4, MATRIX_1:38;
[1,i] in Indices ((SwapDiagonal K,n,j0) * (A @ )) by A4, A5, MATRIX_1:38;
hence (A * (SwapDiagonal K,n,j0)) * i,1 = ((SwapDiagonal K,n,j0) * (A @ )) * 1,i by A2, MATRIX_1:def 7
.= (A @ ) * j0,i by A1, A4, Th48
.= A * i,j0 by A7, 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 that
A8: ( j <> 1 & j <> j0 ) and
A9: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: (A * (SwapDiagonal K,n,j0)) * i,j = A * i,j
A10: [i,j] in Indices A by A9, MATRIX_1:38;
[j,i] in Indices ((SwapDiagonal K,n,j0) * (A @ )) by A9, MATRIX_1:38;
hence (A * (SwapDiagonal K,n,j0)) * i,j = ((SwapDiagonal K,n,j0) * (A @ )) * j,i by A2, MATRIX_1:def 7
.= (A @ ) * j,i by A1, A8, A9, Th48
.= A * i,j by A10, 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 A3; :: thesis: verum