let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 holds rank f = the_rank_of (AutMt f,b1,b2)
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 holds rank f = the_rank_of (AutMt f,b1,b2)
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 holds rank f = the_rank_of (AutMt f,b1,b2)
let b2 be OrdBasis of V2; :: thesis: for f being linear-transformation of V1,V2 holds rank f = the_rank_of (AutMt f,b1,b2)
let f be linear-transformation of V1,V2; :: thesis: rank f = the_rank_of (AutMt f,b1,b2)
set A = AutMt f,b1,b2;

per cases ( len b1 = 0 or ( len b1 > 0 & len b2 = 0 ) or ( len b1 > 0 & len b2 > 0 ) ) ;

suppose len b1 = 0 ; :: thesis: rank f = the_rank_of (AutMt f,b1,b2)

then ( len (AutMt f,b1,b2) = 0 & the_rank_of (AutMt f,b1,b2) <= len (AutMt f,b1,b2) & dim V1 = 0 & dim V1 = (rank f) + (nullity f) ) by Th21, MATRIX13:74, MATRIX_1:def 3, RANKNULL:44;
then ( the_rank_of (AutMt f,b1,b2) = 0 & rank f = 0 ) ;
hence rank f = the_rank_of (AutMt f,b1,b2) ; :: thesis: verum

end;

suppose ( len b1 > 0 & len b2 = 0 ) ; :: thesis: rank f = the_rank_of (AutMt f,b1,b2)

then ( width (AutMt f,b1,b2) = 0 & the_rank_of (AutMt f,b1,b2) <= width (AutMt f,b1,b2) & dim (im f) <= dim V2 & dim V2 = 0 ) by Th21, MATRIX13:74, MATRIX_1:24, VECTSP_9:29;
then ( the_rank_of (AutMt f,b1,b2) = 0 & dim (im f) = 0 ) ;
hence rank f = the_rank_of (AutMt f,b1,b2) ; :: thesis: verum

end;

suppose A1: ( len b1 > 0 & len b2 > 0 ) ; :: thesis: rank f = the_rank_of (AutMt f,b1,b2)

A2: (rank f) + (nullity f) = dim V1 by RANKNULL:44
.= len b1 by Th21 ;
nullity f = nullity (Mx2Tran (AutMt f,b1,b2),b1,b2) by Th34
.= (len b1) - (the_rank_of (AutMt f,b1,b2)) by A1, Lm7 ;
hence rank f = the_rank_of (AutMt f,b1,b2) by A2; :: thesis: verum

end;

end;