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

per cases ;

suppose A1: len b1 = 0 ; :: thesis:

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:

end;

suppose A2: ( len b1 > 0 & len b2 = 0 ) ; :: thesis:

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:

end;

suppose A4: ( len b1 > 0 & len b2 > 0 ) ; :: thesis:

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:

end;

end;