let K be Field; :: thesis: for A, B being Matrix of K st len A = len B & len A = the_rank_of A holds
the_rank_of A = the_rank_of (A ^^ B)
let A, B be Matrix of K; :: thesis: ( len A = len B & len A = the_rank_of A implies the_rank_of A = the_rank_of (A ^^ B) )
assume that
A1: len A = len B and
A2: len A = the_rank_of A ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by A1, MATRIX_0:51;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
A3: ( the_rank_of (A9 ^^ B9) <= len (A9 ^^ B9) & len (A9 ^^ B9) = len A ) by MATRIX13:74, MATRIX_0:def 2;
the_rank_of (A9 ^^ B9) >= len A by A1, A2, Th20;
hence the_rank_of A = the_rank_of (A ^^ B) by A2, A3, XXREAL_0:1; :: thesis: verum