theorem canLininj: :: VECTSP13:22

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds
( canLinTrans f is one-to-one iff ( rng f is linearly-independent & f is one-to-one ) )