let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st A <> 0. K,n holds
ex B, C being Matrix of n,K st
( B is invertible & C is invertible & ((B * A) * C) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((B * A) * C) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((B * A) * C) * 1,j = 0. K ) )
let K be Field; :: thesis: for A being Matrix of n,K st A <> 0. K,n holds
ex B, C being Matrix of n,K st
( B is invertible & C is invertible & ((B * A) * C) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((B * A) * C) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((B * A) * C) * 1,j = 0. K ) )
let A be Matrix of n,K; :: thesis: ( A <> 0. K,n implies ex B, C being Matrix of n,K st
( B is invertible & C is invertible & ((B * A) * C) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((B * A) * C) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((B * A) * C) * 1,j = 0. K ) ) )
assume A <> 0. K,n ; :: thesis: ex B, C being Matrix of n,K st
( B is invertible & C is invertible & ((B * A) * C) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((B * A) * C) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((B * A) * C) * 1,j = 0. K ) )
then consider i0, j0 being Element of NAT such that
A1: ( 1 <= i0 & i0 <= n ) and
A2: ( 1 <= j0 & j0 <= n ) and
A3: A * i0,j0 <> 0. K by Th52;
set A3 = ((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0);
set A2 = (SwapDiagonal K,n,i0) * A;
1 <= n by A1, XXREAL_0:2;
then (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0)) * 1,1 = ((SwapDiagonal K,n,i0) * A) * 1,j0 by A2, Th51
.= A * i0,j0 by A1, A2, Th48 ;
then consider P, Q being Matrix of n,K such that
A4: P is invertible and
A5: Q is invertible and
A6: ( ((P * (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0))) * Q) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((P * (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0))) * Q) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((P * (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0))) * Q) * 1,j = 0. K ) ) by A1, A3, Th41;
set B0 = P * (SwapDiagonal K,n,i0);
set C0 = (SwapDiagonal K,n,j0) * Q;
SwapDiagonal K,n,i0 is invertible by A1, Th49;
then A7: P * (SwapDiagonal K,n,i0) is invertible by A4, MATRIX_6:37;
SwapDiagonal K,n,j0 is invertible by A2, Th49;
then A8: (SwapDiagonal K,n,j0) * Q is invertible by A5, MATRIX_6:37;
((P * (SwapDiagonal K,n,i0)) * A) * ((SwapDiagonal K,n,j0) * Q) = (P * ((SwapDiagonal K,n,i0) * A)) * ((SwapDiagonal K,n,j0) * Q) by Th17
.= ((P * ((SwapDiagonal K,n,i0) * A)) * (SwapDiagonal K,n,j0)) * Q by Th17
.= (P * (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0))) * Q by Th17 ;
hence ex B, C being Matrix of n,K st
( B is invertible & C is invertible & ((B * A) * C) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((B * A) * C) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((B * A) * C) * 1,j = 0. K ) ) by A6, A7, A8; :: thesis: verum