let F be Field; :: thesis: 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 ) )
let U be non trivial finite-dimensional VectSp of F; :: thesis: 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 ) )
let V be finite-dimensional VectSp of F; :: thesis: 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 ) )
let B be Basis of U; :: thesis: 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 ) )
let f be Function of B,V; :: thesis: ( canLinTrans f is one-to-one iff ( rng f is linearly-independent & f is one-to-one ) )

now :: thesis: ( canLinTrans f is one-to-one implies ( rng f is linearly-independent & f is one-to-one ) )

assume A: canLinTrans f is one-to-one ; :: thesis: ( rng f is linearly-independent & f is one-to-one )
f = (canLinTrans f) | B by defcl;
hence ( rng f is linearly-independent & f is one-to-one ) by A, FUNCT_1:52, canLininjrngA; :: thesis: verum

end;

hence ( canLinTrans f is one-to-one iff ( rng f is linearly-independent & f is one-to-one ) ) by canLininjrngB; :: thesis: verum