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 A1: len b1 = 0 ; :: thesis: rank f = the_rank_of (AutMt (f,b1,b2))

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

end;

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

then width (AutMt (f,b1,b2)) = 0 by MATRIX_0:23;
then A3: the_rank_of (AutMt (f,b1,b2)) = 0 by MATRIX13:74;
dim V2 = 0 by A2, Th21;
hence rank f = the_rank_of (AutMt (f,b1,b2)) by A3, VECTSP_9:25; :: thesis: verum

end;

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

A5: (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 A4, Lm7 ;
hence rank f = the_rank_of (AutMt (f,b1,b2)) by A5; :: thesis: verum

end;

end;