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

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