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 A1, MATRIX_3:def 4;
A4: width (B * A) = width A by A1, MATRIX_3:def 4;
A5: ( len A = n & width A = n ) by MATRIX_1:25;

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 A1, A4, A5, MATRIX_2:12;
A8: Det (A @ ) <> 0. K by A2, MATRIXR2:43;
thus the_rank_of (B * A) = the_rank_of ((B * A) @ ) by MATRIX13:84
.= the_rank_of ((A @ ) * (B @ )) by A1, A4, A6, MATRIX_3:24
.= the_rank_of (B @ ) by A1, A8, A7, Th75
.= the_rank_of B by MATRIX13:84 ; :: thesis: verum

end;

end;