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 A1: ( width B = len A & Det A <> 0. K ) ; :: thesis: the_rank_of (B * A) = the_rank_of B
set BA = B * A;
A2: ( len (B * A) = len B & width (B * A) = width A & len A = n & width A = n ) by A1, MATRIX_1:25, MATRIX_3:def 4;

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, A2, Lm3; :: thesis: verum

end;

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

then A4: ( Det (A @ ) <> 0. K & width (A @ ) = len A & len (B @ ) = width B ) by A1, A2, MATRIXR2:43, MATRIX_2:12;
thus the_rank_of (B * A) = the_rank_of ((B * A) @ ) by MATRIX13:84
.= the_rank_of ((A @ ) * (B @ )) by A1, A2, A3, MATRIX_3:24
.= the_rank_of (B @ ) by A1, A4, Th75
.= the_rank_of B by MATRIX13:84 ; :: thesis: verum

end;

end;