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: ( len (A * B) = len A & 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 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 )

then A3: ( len (A * B) > 0 & width (A * B) > 0 ) by MATRIX13:74;
then ( ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) ) by A1, A2, MATRIX_1:def 4;
then ( Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) & 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 A1, A2, Th72, Th68;
then A4: (width B) - (the_rank_of B) <= (width B) - (the_rank_of (A * B)) by A2, VECTSP_9:29;
set AT = A @ ;
set BT = B @ ;
set BA = (B @ ) * (A @ );
width A > 0 by A1, A3, A2, MATRIX_1:def 4;
then A5: ( width (A @ ) = len A & len (A @ ) = width A & width (B @ ) = len B & len (B @ ) = width B ) by A2, A3, MATRIX_2:12;
then A6: ( len ((B @ ) * (A @ )) = len (B @ ) & width ((B @ ) * (A @ )) = width (A @ ) & (B @ ) * (A @ ) = (A * B) @ ) by A1, A2, A3, MATRIX_3:24, MATRIX_3:def 4;
( ( width (A @ ) = 0 implies len (A @ ) = 0 ) & ( width (B @ ) = 0 implies len (B @ ) = 0 ) & width (B @ ) = len (A @ ) ) by A1, A5, MATRIX_1:def 4;
then ( Space_of_Solutions_of (A @ ) is Subspace of Space_of_Solutions_of ((B @ ) * (A @ )) & dim (Space_of_Solutions_of (A @ )) = (width (A @ )) - (the_rank_of (A @ )) & dim (Space_of_Solutions_of ((B @ ) * (A @ ))) = (width ((B @ ) * (A @ ))) - (the_rank_of ((B @ ) * (A @ ))) ) by Th72, Th68, A6;
then (width (A @ )) - (the_rank_of (A @ )) <= (width (A @ )) - (the_rank_of ((B @ ) * (A @ ))) by A6, VECTSP_9:29;
then the_rank_of (A @ ) >= the_rank_of ((B @ ) * (A @ )) by XREAL_1:12;
then the_rank_of A >= the_rank_of ((B @ ) * (A @ )) by MATRIX13:84;
hence ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B ) by A4, A6, MATRIX13:84, XREAL_1:12; :: thesis: verum

end;

end;