let n be Nat; :: thesis: for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st width A = len B & Det A <> 0. K holds
the_rank_of (A * B) = the_rank_of B
let K be Field; :: thesis: for A being Matrix of n,n,K
for B being Matrix of K st width A = len B & Det A <> 0. K holds
the_rank_of (A * B) = the_rank_of B
let A be Matrix of n,n,K; :: thesis: for B being Matrix of K st width A = len B & Det A <> 0. K holds
the_rank_of (A * B) = the_rank_of B
let B be Matrix of K; :: thesis: ( width A = len B & Det A <> 0. K implies the_rank_of (A * B) = the_rank_of B )
assume that
A1: width A = len B and
A2: Det A <> 0. K ; :: thesis: the_rank_of (A * B) = the_rank_of B
set AB = A * B;
A3: len (A * B) = len A by A1, MATRIX_3:def 4;
A4: ( len A = n & width A = n ) by MATRIX_0:24;
A5: width (A * B) = width B by A1, MATRIX_3:def 4;

per cases ( width (A * B) = 0 or width (A * B) > 0 ) ;

suppose width (A * B) = 0 ; :: thesis: the_rank_of (A * B) = the_rank_of B

hence the_rank_of (A * B) = the_rank_of B by A1, A3, A5, A4, Lm3; :: thesis: verum

end;

suppose A6: width (A * B) > 0 ; :: thesis: the_rank_of (A * B) = the_rank_of B

then ( Space_of_Solutions_of B = Space_of_Solutions_of (A * B) & dim (Space_of_Solutions_of B) = (width B) - (the_rank_of B) ) by A1, A2, A5, Th68, Th74;
then (width B) - (the_rank_of B) = (width B) - (the_rank_of (A * B)) by A5, A6, Th68;
hence the_rank_of (A * B) = the_rank_of B ; :: thesis: verum

end;

end;