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_1:def 3;
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_1:24;
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:29; :: 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;