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:36;
SwapDiagonal (K,n,j0) is invertible by A2, Th49;
then A8: (SwapDiagonal (K,n,j0)) * Q is invertible by A5, MATRIX_6:36;
((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