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

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

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

let B be Matrix of K; :: thesis: ( len A = width B & Det A <> 0. K implies the_rank_of (B * A) = the_rank_of B )
assume that
A1: width B = len A and
A2: Det A <> 0. K ; :: thesis: the_rank_of (B * A) = the_rank_of B
set BA = B * A;
A3: len (B * A) = len B by ;
A4: width (B * A) = width A by ;
A5: ( len A = n & width A = n ) by MATRIX_0:24;
per cases ( width (B * A) = 0 or width (B * A) > 0 ) ;
suppose width (B * A) = 0 ; :: thesis: the_rank_of (B * A) = the_rank_of B
hence the_rank_of (B * A) = the_rank_of B by A1, A3, A4, A5, Lm3; :: thesis: verum
end;
suppose A6: width (B * A) > 0 ; :: thesis: the_rank_of (B * A) = the_rank_of B
then A7: ( width (A @) = len A & len (B @) = width B ) by ;
A8: Det (A @) <> 0. K by ;
thus the_rank_of (B * A) = the_rank_of ((B * A) @) by MATRIX13:84
.= the_rank_of ((A @) * (B @)) by
.= the_rank_of (B @) by A1, A8, A7, Th75
.= the_rank_of B by MATRIX13:84 ; :: thesis: verum
end;
end;