let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st n > 0 & A * 1,1 <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (P * A) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * 1,j = 0. K holds
(P * A) * 1,j = 0. K ) )
let K be Field; :: thesis: for A being Matrix of n,K st n > 0 & A * 1,1 <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (P * A) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * 1,j = 0. K holds
(P * A) * 1,j = 0. K ) )
let A be Matrix of n,K; :: thesis: ( n > 0 & A * 1,1 <> 0. K implies ex P being Matrix of n,K st
( P is invertible & (P * A) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * 1,j = 0. K holds
(P * A) * 1,j = 0. K ) ) )
assume that
A1: n > 0 and
A2: A * 1,1 <> 0. K ; :: thesis: ex P being Matrix of n,K st
( P is invertible & (P * A) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * 1,j = 0. K holds
(P * A) * 1,j = 0. K ) )
set B = A @ ;
A3: 0 + 1 <= n by A1, NAT_1:13;
then [1,1] in Indices A by MATRIX_1:38;
then (A @ ) * 1,1 = A * 1,1 by MATRIX_1:def 7;
then consider P0 being Matrix of n,K such that
A4: P0 is invertible and
A5: ((A @ ) * P0) * 1,1 = 1. K and
A6: for i being Element of NAT st 1 < i & i <= n holds
((A @ ) * P0) * 1,i = 0. K and
A7: for j being Element of NAT st 1 < j & j <= n & (A @ ) * j,1 = 0. K holds
((A @ ) * P0) * j,1 = 0. K by A1, A2, Th39;
A8: [1,1] in Indices ((A @ ) * P0) by A3, MATRIX_1:38;
A9: for j being Element of NAT st 1 < j & j <= n & A * 1,j = 0. K holds
((P0 @ ) * A) * 1,j = 0. K

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n & A * 1,j = 0. K implies ((P0 @ ) * A) * 1,j = 0. K )
assume that
A10: ( 1 < j & j <= n ) and
A11: A * 1,j = 0. K ; :: thesis: ((P0 @ ) * A) * 1,j = 0. K
[1,j] in Indices A by A3, A10, MATRIX_1:38;
then (A @ ) * j,1 = A * 1,j by MATRIX_1:def 7;
then A12: ((A @ ) * P0) * j,1 = 0. K by A7, A10, A11;
[j,1] in Indices ((A @ ) * P0) by A3, A10, MATRIX_1:38;
then (((A @ ) * P0) @ ) * 1,j = 0. K by A12, MATRIX_1:def 7;
then ((P0 @ ) * ((A @ ) @ )) * 1,j = 0. K by Th30;
hence ((P0 @ ) * A) * 1,j = 0. K by MATRIXR2:29; :: thesis: verum

end;

A13: for i being Element of NAT st 1 < i & i <= n holds
((P0 @ ) * A) * i,1 = 0. K

proof

let i be Element of NAT ; :: thesis: ( 1 < i & i <= n implies ((P0 @ ) * A) * i,1 = 0. K )
assume ( 1 < i & i <= n ) ; :: thesis: ((P0 @ ) * A) * i,1 = 0. K
then A14: ( [1,i] in Indices ((A @ ) * P0) & ((A @ ) * P0) * 1,i = 0. K ) by A3, A6, MATRIX_1:38;
((A @ ) * P0) @ = (P0 @ ) * ((A @ ) @ ) by Th30
.= (P0 @ ) * A by MATRIXR2:29 ;
hence ((P0 @ ) * A) * i,1 = 0. K by A14, MATRIX_1:def 7; :: thesis: verum

end;

A15: P0 @ is invertible by A4, Th31;
((P0 @ ) * A) * 1,1 = ((P0 @ ) * ((A @ ) @ )) * 1,1 by MATRIXR2:29
.= (((A @ ) * P0) @ ) * 1,1 by Th30
.= 1. K by A5, A8, MATRIX_1:def 7 ;
hence ex P being Matrix of n,K st
( P is invertible & (P * A) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * i,1 = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * 1,j = 0. K holds
(P * A) * 1,j = 0. K ) ) by A13, A15, A9; :: thesis: verum