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

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

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

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

end;

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

hence ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m by A1, Lm1; :: thesis: verum

end;

end;