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 f is one-to-one & rng f is linearly-independent holds
canLinTrans 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 st f is one-to-one & rng f is linearly-independent holds
canLinTrans 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 st f is one-to-one & rng f is linearly-independent holds
canLinTrans f is one-to-one
let B be Basis of U; :: thesis: for f being Function of B,V st f is one-to-one & rng f is linearly-independent holds
canLinTrans f is one-to-one
let f be Function of B,V; :: thesis: ( f is one-to-one & rng f is linearly-independent implies canLinTrans f is one-to-one )
assume AS: f is one-to-one ; :: thesis: ( not rng f is linearly-independent or canLinTrans f is one-to-one )
set T = canLinTrans f;
H0: the carrier of (Lin B) = { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
H1: Lin B = ModuleStr(# the carrier of U, the addF of U, the ZeroF of U, the lmult of U #) by VECTSP_7:def 3;
assume B0: rng f is linearly-independent ; :: thesis: canLinTrans f is one-to-one

now :: thesis: for x1, x2 being object st x1 in the carrier of U & x2 in the carrier of U & (canLinTrans f) . x1 = (canLinTrans f) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of U & x2 in the carrier of U & (canLinTrans f) . x1 = (canLinTrans f) . x2 implies x1 = x2 )
assume B1: ( x1 in the carrier of U & x2 in the carrier of U & (canLinTrans f) . x1 = (canLinTrans f) . x2 ) ; :: thesis: x1 = x2
then reconsider v1 = x1, v2 = x2 as Element of U ;
v1 in Lin B by H1;
then consider l1 being Linear_Combination of B such that
B2: Sum l1 = v1 by H0;
v2 in Lin B by H1;
then consider l2 being Linear_Combination of B such that
B3: Sum l2 = v2 by H0;
B4: v1 - v2 = Sum (l1 - l2) by B2, B3, VECTSP_6:47;
B5: (canLinTrans f) . ((Sum l1) - (Sum l2)) = (canLinTrans f) . (Sum (l1 - l2)) by VECTSP_6:47
.= ((canLinTrans f) . v1) - ((canLinTrans f) . v2) by B4, RANKNULL:8
.= 0. V by B1, RLVECT_1:5 ;
reconsider l3 = l1 - l2 as Linear_Combination of B by VECTSP_6:42;
( {} c= rng f & Carrier (ZeroLC V) = {} ) by VECTSP_6:def 3;
then B7: ZeroLC V is Linear_Combination of rng f by VECTSP_6:def 4;
(canLinTrans f) . ((Sum l1) - (Sum l2)) = ((canLinTrans f) . (Sum l1)) - ((canLinTrans f) . (Sum l2)) by RANKNULL:8
.= (Sum (f (#) l1)) - ((canLinTrans f) . (Sum l2)) by CLS
.= (Sum (f (#) l1)) - (Sum (f (#) l2)) by CLS
.= Sum (f (#) l3) by lemminus ;
then B9: Sum (f (#) l3) = Sum (ZeroLC V) by B5, VECTSP_6:15;

now :: thesis: for u being Element of U holds not u in Carrier (l1 - l2)

let u be Element of U; :: thesis: not u in Carrier (l1 - l2)
assume u in Carrier (l1 - l2) ; :: thesis: contradiction
then B12: (l1 - l2) . u <> 0. F by VECTSP_6:2;
then B13: ((f (#) l3) (#) f) . u <> 0. F by AS, XXX3;

per cases ( u in B or not u in B ) ;

suppose S: u in B ; :: thesis: contradiction

then B10: (f (#) l3) . (f . u) <> 0. F by B13, defK1;
dom f = B by FUNCT_2:def 1;
then f . u in rng f by S, FUNCT_1:3;
then f . u in Carrier (f (#) l3) by B10;
hence contradiction by B9, B7, B0, FIELD_7:6, VECTSP_6:def 3; :: thesis: verum

end;

suppose S: not u in B ; :: thesis: contradiction

( Carrier l1 c= B & Carrier l2 c= B ) by VECTSP_6:def 4;
then ( l1 . u = 0. F & l2 . u = 0. F ) by S, VECTSP_6:2;
then (l1 . u) - (l2 . u) = 0. F ;
hence contradiction by B12, VECTSP_6:40; :: thesis: verum

end;

end;

end;

then Carrier (l1 - l2) is empty ;
then l1 - l2 = ZeroLC U by VECTSP_6:def 3;
then - (- l2) = - (- l1) by VECTSP_6:37;
hence x1 = x2 by B2, B3; :: thesis: verum

end;

hence canLinTrans f is one-to-one by FUNCT_2:19; :: thesis: verum