let K be Field; :: thesis: for A, B being Matrix of K st width A = len B holds
( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )

let A, B be Matrix of K; :: thesis: ( width A = len B implies ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B ) )
assume A1: width A = len B ; :: thesis: ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )
set AB = A * B;
A2: width (A * B) = width B by ;
per cases ( the_rank_of (A * B) = 0 or the_rank_of (A * B) > 0 ) ;
suppose the_rank_of (A * B) = 0 ; :: thesis: ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )
end;
suppose A3: the_rank_of (A * B) > 0 ; :: thesis: ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )
set AT = A @ ;
A4: width (A * B) > 0 by ;
then A5: width A > 0 by ;
then A6: len (A @) = width A by MATRIX_0:54;
set BT = B @ ;
set BA = (B @) * (A @);
width (A @) = len A by ;
then A7: ( width (A @) = 0 implies len (A @) = 0 ) by ;
then A8: dim () = (width (A @)) - (the_rank_of (A @)) by Th68;
A9: width (B @) = len B by ;
then ( width (B @) = 0 implies len (B @) = 0 ) by ;
then A10: Space_of_Solutions_of (A @) is Subspace of Space_of_Solutions_of ((B @) * (A @)) by A1, A6, A9, A7, Th72;
A11: width ((B @) * (A @)) = width (A @) by ;
then dim (Space_of_Solutions_of ((B @) * (A @))) = (width ((B @) * (A @))) - (the_rank_of ((B @) * (A @))) by ;
then (width (A @)) - (the_rank_of (A @)) <= (width (A @)) - (the_rank_of ((B @) * (A @))) by ;
then the_rank_of (A @) >= the_rank_of ((B @) * (A @)) by XREAL_1:10;
then A12: the_rank_of A >= the_rank_of ((B @) * (A @)) by MATRIX13:84;
( width A = 0 implies len A = 0 ) by ;
then A13: Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) by A1, A2, A4, Th72;
( dim = () - () & dim (Space_of_Solutions_of (A * B)) = (width (A * B)) - (the_rank_of (A * B)) ) by A2, A4, Th68;
then A14: (width B) - () <= () - (the_rank_of (A * B)) by ;
(B @) * (A @) = (A * B) @ by ;
hence ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B ) by ; :: thesis: verum
end;
end;