let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
let V, W be VectSp of F; :: 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 Subspace of ker T by VECTSP_4:39;
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 not v in Z ; :: thesis: contradiction
then A3: not v = 0. V by VECTSP_4:35;
A4: ( T . (0. V) = 0. W & dom T = [#] V ) by Th7, Th9;
reconsider v = v as Element of V by VECTSP_4:10;
T . v = 0. W by A2, Th10;
hence contradiction by A1, A3, A4; :: thesis: verum

end;

hence ker T = (0). V by VECTSP_4:32; :: thesis: verum