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_1:def 4;
then A6: len (A @ ) = width A by MATRIX_2:12;
set BT = B @ ;
set BA = (B @ ) * (A @ );
width (A @ ) = len A by A5, MATRIX_2:12;
then A7: ( width (A @ ) = 0 implies len (A @ ) = 0 ) by A5, MATRIX_1:def 4;
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_2:12;
then ( width (B @ ) = 0 implies len (B @ ) = 0 ) by A2, A4, MATRIX_1:def 4;
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_2:12;
then (width (A @ )) - (the_rank_of (A @ )) <= (width (A @ )) - (the_rank_of ((B @ ) * (A @ ))) by A11, A10, A8, VECTSP_9:29;
then the_rank_of (A @ ) >= the_rank_of ((B @ ) * (A @ )) by XREAL_1:12;
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_1:def 4;
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:29;
(B @ ) * (A @ ) = (A * B) @ by A1, A2, A4, MATRIX_3:24;
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:12; :: thesis: verum

end;

end;