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 A1, MATRIX_3:def 4;

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 )

hence ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B ) ; :: thesis: verum

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 A3, MATRIX13:74;
then A5: width A > 0 by A1, A2, MATRIX_0:def 3;
then A6: len (A @) = width A by MATRIX_0:54;
set BT = B @ ;
set BA = (B @) * (A @);
width (A @) = len A by A5, MATRIX_0:54;
then A7: ( width (A @) = 0 implies len (A @) = 0 ) by A5, MATRIX_0:def 3;
then A8: dim (Space_of_Solutions_of (A @)) = (width (A @)) - (the_rank_of (A @)) by Th68;
A9: width (B @) = len B by A2, A4, MATRIX_0:54;
then ( width (B @) = 0 implies len (B @) = 0 ) by A2, A4, MATRIX_0:def 3;
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 A1, A6, A9, MATRIX_3:def 4;
then dim (Space_of_Solutions_of ((B @) * (A @))) = (width ((B @) * (A @))) - (the_rank_of ((B @) * (A @))) by A5, A7, Th68, MATRIX_0:54;
then (width (A @)) - (the_rank_of (A @)) <= (width (A @)) - (the_rank_of ((B @) * (A @))) by A11, A10, A8, VECTSP_9:25;
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 A1, A2, A4, MATRIX_0:def 3;
then A13: Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) by A1, A2, A4, Th72;
( dim (Space_of_Solutions_of B) = (width B) - (the_rank_of B) & 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 B) <= (width B) - (the_rank_of (A * B)) by A2, A13, VECTSP_9:25;
(B @) * (A @) = (A * B) @ by A1, A2, A4, MATRIX_3:22;
hence ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B ) by A14, A12, MATRIX13:84, XREAL_1:10; :: thesis: verum

end;

end;