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 A1: T is one-to-one ; :: thesis: dim V = rank T
ker T = (0). V by A1, Th15;
then A2: nullity T = 0 by Th16;
dim V = (rank T) + (nullity T) by Th44
.= rank T by A2 ;
hence dim V = rank T ; :: thesis: verum