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, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A2: ( x in dom f & y in dom f ) and
A3: f . x = f . y ; :: thesis: x = y
reconsider x9 = x, y9 = y as Element of V1 by A2, FUNCT_2:def 1;
x9 - y9 in ker f by A3, RANKNULL:17;
then x9 - y9 in the carrier of ((0). V1) by A1;
then x9 - y9 in {(0. V1)} by VECTSP_4:def 3;
then x9 + (- y9) = 0. V1 by TARSKI:def 1;
hence x = - (- y9) by VECTSP_1:16
.= y by RLVECT_1:17 ;
:: thesis: verum

end;

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