let n, m be Nat; :: thesis: for K being Field
for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
let K be Field; :: thesis: for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
let A be Matrix of n,m,K; :: thesis: ( the_rank_of A = m implies ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n )
assume A1: the_rank_of A = m ; :: thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
A2: len A = n by MATRIX_0:def 2;

per cases ( m = 0 or m > 0 ) ;

suppose A3: m = 0 ; :: thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n

then n -' m = n - m by XREAL_0:def 2;
then reconsider ONE = 1. (K,n) as Matrix of n,n -' m,K by A3;
A4: len (1. (K,n)) = n by MATRIX_0:24;
Det (1. (K,n)) <> 0. K by LAPLACE:34;
then A5: the_rank_of ONE = n by MATRIX13:83;
width A = m by A3, MATRIX13:1;
then A ^^ ONE = ONE by A2, A3, A4, MATRIX15:22;
hence ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n by A5; :: thesis: verum

end;

suppose A6: m > 0 ; :: thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n

n - m >= 0 by A1, A2, MATRIX13:74, XREAL_1:48;
then A7: n -' m = n - m by XREAL_0:def 2;
A8: n > 0 by A1, A2, A6, MATRIX13:74;
then A9: width A = m by MATRIX13:1;

per cases ( n = m or n <> m ) ;

suppose A10: n = m ; :: thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n

take B = the Matrix of n,n -' m,K; :: thesis: the_rank_of (A ^^ B) = n
( len B = n & width B = 0 ) by A6, A7, A10, MATRIX_0:23;
hence the_rank_of (A ^^ B) = n by A1, A2, A10, MATRIX15:22; :: thesis: verum

end;

suppose A11: n <> m ; :: thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n

A12: width (A @) = n by A2, A6, A9, MATRIX_0:54;
len (A @) = m by A6, A9, MATRIX_0:54;
then reconsider A1 = A @ as Matrix of m,n,K by A12, MATRIX_0:51;
the_rank_of A1 = m by A1, MATRIX13:84;
then consider B being Matrix of n -' m,n,K such that
A13: the_rank_of (A1 ^ B) = n by Th16;
A14: n -' m <> 0 by A7, A11;
then A15: width B = n by MATRIX13:1;
then A16: len (B @) = n by A8, MATRIX_0:54;
len B = n -' m by A14, MATRIX13:1;
then width (B @) = n -' m by A8, A15, MATRIX_0:54;
then reconsider B1 = B @ as Matrix of n,n -' m,K by A16, MATRIX_0:51;
A1 @ = A by A2, A6, A8, A9, MATRIX_0:57;
then A17: (A1 ^ B) @ = A ^^ B1 by A12, A15, MATRLIN:28;
the_rank_of ((A1 ^ B) @) = n by A13, MATRIX13:84;
hence ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n by A17; :: thesis: verum

end;

end;

end;

end;