let F be Field; :: thesis: for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
let V, W be finite-dimensional VectSp of F; :: thesis: for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
let T be linear-transformation of V,W; :: thesis: ( T is one-to-one implies dim V = rank T )
assume T is one-to-one ; :: thesis: dim V = rank T
then ker T = (0). V by Th15;
then A1: nullity T = 0 by Th16;
dim V = (rank T) + (nullity T) by Th44
.= rank T by A1 ;
hence dim V = rank T ; :: thesis: verum