let V, W be free finite-rank Z_Module; :: thesis: for T being linear-transformation of V,W st T is one-to-one holds
rank V = rank T
let T be linear-transformation of V,W; :: thesis: ( T is one-to-one implies rank V = rank T )
assume T is one-to-one ; :: thesis: rank V = rank T
then ker T = (0). V by ZMODUL05:25;
then A1: nullity T = 0 by ZMODUL05:26;
rank V = (rank T) + (nullity T) by Th44
.= rank T by A1 ;
hence rank V = rank T ; :: thesis: verum