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 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;
set AB = A' ^^ B';

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 len A > 0 ; :: thesis: ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) )

then A2: ( width (A' ^^ B') = (width A) + (width B) & Indices (A' ^^ B') = [:(Seg (len A)),(Seg ((width A) + (width B))):] ) by MATRIX_1:24;
then A3: ( Segm (A' ^^ B'),(Seg (len A)),(Seg (width A)) = A & Segm (A' ^^ B'),(Seg (len A)),((Seg (width (A' ^^ B'))) \ (Seg (width A))) = B ) by Th19;
width A <= width (A' ^^ B') by A2, NAT_1:11;
then ( Seg (width A) c= Seg (width (A' ^^ B')) & (Seg (width (A' ^^ B'))) \ (Seg (width A)) c= Seg (width (A' ^^ B')) ) by FINSEQ_1:7, XBOOLE_1:36;
then ( [:(Seg (len A)),(Seg (width A)):] c= Indices (A' ^^ B') & [:(Seg (len A)),((Seg (width (A' ^^ B'))) \ (Seg (width A))):] c= Indices (A' ^^ B') ) by A2, ZFMISC_1:118;
hence ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) ) by A3, MATRIX13:79; :: thesis: verum

end;

end;