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, Q being Matrix of n,K st
( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((P * A) * Q) * (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, Q being Matrix of n,K st
( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((P * A) * Q) * (1,j) = 0. K ) )
let A be Matrix of n,K; :: thesis: ( n > 0 & A * (1,1) <> 0. K implies ex P, Q being Matrix of n,K st
( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((P * A) * Q) * (1,j) = 0. K ) ) )
assume that
A1: n > 0 and
A2: A * (1,1) <> 0. K ; :: thesis: ex P, Q being Matrix of n,K st
( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((P * A) * Q) * (1,j) = 0. K ) )
consider P being Matrix of n,K such that
A3: P is invertible and
A4: (P * A) * (1,1) = 1. K and
A5: for i being Element of NAT st 1 < i & i <= n holds
(P * A) * (i,1) = 0. K and
for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
(P * A) * (1,j) = 0. K by A1, A2, Th40;
consider Q being Matrix of n,K such that
A6: ( Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
((P * A) * Q) * (1,j) = 0. K ) ) and
A7: for i being Element of NAT st 1 < i & i <= n & (P * A) * (i,1) = 0. K holds
((P * A) * Q) * (i,1) = 0. K by A1, A4, Th39;
for i being Element of NAT st 1 < i & i <= n holds
((P * A) * Q) * (i,1) = 0. K

proof

let i be Element of NAT ; :: thesis: ( 1 < i & i <= n implies ((P * A) * Q) * (i,1) = 0. K )
assume A8: ( 1 < i & i <= n ) ; :: thesis: ((P * A) * Q) * (i,1) = 0. K
then (P * A) * (i,1) = 0. K by A5;
hence ((P * A) * Q) * (i,1) = 0. K by A7, A8; :: thesis: verum

end;

hence ex P, Q being Matrix of n,K st
( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds
((P * A) * Q) * (1,j) = 0. K ) ) by A3, A6; :: thesis: verum