let K be Field; :: thesis: for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2 holds
( f is one-to-one iff ker f = (0). V1 )
let V1, V2 be VectSp of K; :: thesis: for f being linear-transformation of V1,V2 holds
( f is one-to-one iff ker f = (0). V1 )
let f be linear-transformation of V1,V2; :: thesis: ( f is one-to-one iff ker f = (0). V1 )
( ker f = (0). V1 implies f is one-to-one )

proof

assume A1: ker f = (0). V1 ; :: thesis: f is one-to-one
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A2: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
reconsider x' = x, y' = y as Element of V1 by A2, FUNCT_2:def 1;
x' - y' in ker f by A2, RANKNULL:17;
then x' - y' in the carrier of ((0). V1) by A1, STRUCT_0:def 5;
then x' - y' in {(0. V1)} by VECTSP_4:def 3;
then x' + (- y') = 0. V1 by TARSKI:def 1;
hence x = - (- y') by VECTSP_1:63
.= y by RLVECT_1:30 ;
:: thesis: verum

end;

hence ( f is one-to-one iff ker f = (0). V1 ) by RANKNULL:15; :: thesis: verum