let K be Field; :: thesis: for A, B being Matrix of 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 ; :: 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 B' = B as Matrix of the carrier of K, len A, by A1, MATRIX_2:7;
reconsider A' = A as Matrix of the carrier of K, len A, by MATRIX_2:7;
A3: ( the_rank_of (A' ^^ B') <= len (A' ^^ B') & len (A' ^^ B') = len A ) by MATRIX13:74, MATRIX_1:def 3;
the_rank_of (A' ^^ B') >= len A by A1, A2, Th20;
hence the_rank_of A = the_rank_of (A ^^ B) by A2, A3, XXREAL_0:1; :: thesis: verum