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 A1: ( len A = len B & len A = the_rank_of A ) ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
set L = len A;
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;
reconsider B' = B as Matrix of len A, width B,K by A1, MATRIX_2:7;
( the_rank_of (A' ^^ B') <= len (A' ^^ B') & len (A' ^^ B') = len A & the_rank_of (A' ^^ B') >= len A ) by A1, Th20, MATRIX13:74, MATRIX_1:def 3;
hence the_rank_of A = the_rank_of (A ^^ B) by A1, XXREAL_0:1; :: thesis: verum