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 ;
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) )
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 ())) = A by Th19;
A4: Indices (A9 ^^ B9) = [:(Seg (len A)),(Seg (() + ())):] by ;
A5: width (A9 ^^ B9) = () + () by ;
then width A <= width (A9 ^^ B9) by NAT_1:11;
then Seg () c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;
then A6: [:(Seg (len A)),(Seg ()):] c= Indices (A9 ^^ B9) by ;
(Seg (width (A9 ^^ B9))) \ (Seg ()) c= Seg (width (A9 ^^ B9)) by XBOOLE_1:36;
then A7: [:(Seg (len A)),((Seg (width (A9 ^^ B9))) \ (Seg ())):] c= Indices (A9 ^^ B9) by ;
Segm ((A9 ^^ B9),(Seg (len A)),((Seg (width (A9 ^^ B9))) \ (Seg ()))) = B by ;
hence ( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) ) by ; :: thesis: verum
end;
end;