let K be Field; :: thesis: for A, B being Matrix of K st len A = len B holds
( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) )
let A, B be Matrix of K; :: thesis: ( len A = len B implies ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) ) )
assume A1: len A = len B ; :: thesis: ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= 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;
set AB = A9 ^^ B9;

per cases ( len A = 0 or len A > 0 ) ;

suppose len A = 0 ; :: thesis: ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) )

hence ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) ) by A1, MATRIX13:74; :: thesis: verum

end;

suppose A2: len A > 0 ; :: thesis: ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) )

A3: Segm ((A9 ^^ B9),(Seg (len A)),(Seg (width A))) = A by Th19;
A4: Indices (A9 ^^ B9) = [:(Seg (len A)),(Seg ((width A) + (width B))):] by A2, MATRIX_0:23;
A5: width (A9 ^^ B9) = (width A) + (width B) by A2, MATRIX_0:23;
then width A <= width (A9 ^^ B9) by NAT_1:11;
then Seg (width A) c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;
then A6: [:(Seg (len A)),(Seg (width A)):] c= Indices (A9 ^^ B9) by A5, A4, ZFMISC_1:95;
(Seg (width (A9 ^^ B9))) \ (Seg (width A)) c= Seg (width (A9 ^^ B9)) by XBOOLE_1:36;
then A7: [:(Seg (len A)),((Seg (width (A9 ^^ B9))) \ (Seg (width A))):] c= Indices (A9 ^^ B9) by A5, A4, ZFMISC_1:95;
Segm ((A9 ^^ B9),(Seg (len A)),((Seg (width (A9 ^^ B9))) \ (Seg (width A)))) = B by A5, Th19;
hence ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) ) by A3, A6, A7, MATRIX13:79; :: thesis: verum

end;

end;