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 st canLinTrans f is one-to-one holds
rng f is linearly-independent
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 st canLinTrans f is one-to-one holds
rng f is linearly-independent
let V be finite-dimensional VectSp of F; :: thesis: for B being Basis of U
for f being Function of B,V st canLinTrans f is one-to-one holds
rng f is linearly-independent
let B be Basis of U; :: thesis: for f being Function of B,V st canLinTrans f is one-to-one holds
rng f is linearly-independent
let f be Function of B,V; :: thesis: ( canLinTrans f is one-to-one implies rng f is linearly-independent )
set T = canLinTrans f;
assume A0: canLinTrans f is one-to-one ; :: thesis: rng f is linearly-independent
f = (canLinTrans f) | B by defcl;
then A1: f is one-to-one by A0, FUNCT_1:52;

now :: thesis: for l2 being Linear_Combination of rng f st Sum l2 = 0. V holds
Carrier l2 = {}

let l2 be Linear_Combination of rng f; :: thesis: ( Sum l2 = 0. V implies Carrier l2 = {} )
assume A2: Sum l2 = 0. V ; :: thesis: Carrier l2 = {}

now :: thesis: not Carrier l2 <> {}

assume A3: Carrier l2 <> {} ; :: thesis: contradiction
set o = the Element of Carrier l2;
the Element of Carrier l2 in Carrier l2 by A3;
then consider v being Element of V such that
A4: ( v = the Element of Carrier l2 & l2 . v <> 0. F ) ;
( Carrier (ZeroLC U) = {} & {} c= B ) by VECTSP_6:def 3;
then reconsider l0 = ZeroLC U as Linear_Combination of B by VECTSP_6:def 4;
set l1 = l2 (#) f;
(canLinTrans f) . (Sum (l2 (#) f)) = Sum l2 by A1, XXX4a
.= (canLinTrans f) . (0. U) by A2, RANKNULL:9
.= (canLinTrans f) . (Sum (ZeroLC U)) by VECTSP_6:15 ;
then Sum (l2 (#) f) = Sum (ZeroLC U) by A0, FUNCT_2:19;
then A6: l2 (#) f = l0 by FIELD_7:6;
Carrier l2 c= rng f by VECTSP_6:def 4;
then the Element of Carrier l2 in rng f by A3;
then consider x being object such that
A7: ( x in dom f & f . x = v ) by A4, FUNCT_1:def 3;
reconsider u = x as Element of B by A7;
(l2 (#) f) . u <> 0. F by A4, A7, defK1;
then u in Carrier (l2 (#) f) ;
hence contradiction by A6, VECTSP_6:def 3; :: thesis: verum

end;

hence Carrier l2 = {} ; :: thesis: verum

end;

hence rng f is linearly-independent by VECTSP_7:def 1; :: thesis: verum