let V, W be Z_Module; :: thesis: for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
let T be linear-transformation of V,W; :: thesis: ( T is one-to-one implies ker T = (0). V )
reconsider Z = (0). V as Submodule of ker T by ZMODUL01:54;
assume A1: T is one-to-one ; :: thesis: ker T = (0). V
for v being Element of (ker T) holds v in Z

proof

let v be Element of (ker T); :: thesis: v in Z
A2: v in ker T ;
assume AS: not v in Z ; :: thesis: contradiction
A3: ( T . (0. V) = 0. W & dom T = [#] V ) by RANKNULL:7, Th9;
reconsider v = v as Element of V by ZMODUL01:25;
T . v = 0. W by A2, Th10;
then v = 0. V by A1, A3, FUNCT_1:def 4;
then v in {(0. V)} by TARSKI:def 1;
hence contradiction by AS, VECTSP_4:def 3; :: thesis: verum

end;

hence ker T = (0). V by ZMODUL01:149; :: thesis: verum