theorem :: ZMODUL05:25

for V, W being Z_Module
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V by RANKNULL:15;