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 A0: 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 ) )
consider i0, j0 being Element of NAT such that
A4: ( 1 <= i0 & i0 <= n & 1 <= j0 & j0 <= n & A * i0,j0 <> 0. K ) by AA4190, A0;
set A2 = (SwapDiagonal K,n,i0) * A;
B1: 1 <= n by A4, XXREAL_0:2;
B3: (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0)) * 1,1 = ((SwapDiagonal K,n,i0) * A) * 1,j0 by A4, AA4170, B1
.= A * i0,j0 by A4, AA4100 ;
set A3 = ((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0);
consider P, Q being Matrix of n,K such that
A13: ( P is invertible & Q is invertible & ((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 A4, B3, AA3040;
set B0 = P * (SwapDiagonal K,n,i0);
set C0 = (SwapDiagonal K,n,j0) * Q;
A15a: SwapDiagonal K,n,i0 is invertible by A4, AA4150;
A15: P * (SwapDiagonal K,n,i0) is invertible by A13, A15a, MATRIX_6:37;
A15b: SwapDiagonal K,n,j0 is invertible by A4, AA4150;
A17: (SwapDiagonal K,n,j0) * Q is invertible by A13, A15b, 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 AA41
.= ((P * ((SwapDiagonal K,n,i0) * A)) * (SwapDiagonal K,n,j0)) * Q by AA41
.= (P * (((SwapDiagonal K,n,i0) * A) * (SwapDiagonal K,n,j0))) * Q by AA41 ;
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 A15, A17, A13; :: thesis: verum