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;