let F be Field; :: thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let W, V be VectSp of F; :: thesis: for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let T be linear-transformation of V,W; :: thesis: for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let A be Subset of V; :: thesis: for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let B be Basis of V; :: thesis: ( A is Basis of ker T & A c= B implies T | (B \ A) is one-to-one )
assume that
A1: A is Basis of ker T and
A2: A c= B ; :: thesis: T | (B \ A) is one-to-one
reconsider A9 = A as Subset of V ;
set f = T | (B \ A);
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (T | (B \ A)) or not x2 in proj1 (T | (B \ A)) or not (T | (B \ A)) . x1 = (T | (B \ A)) . x2 or x1 = x2 )
assume that
A3: x1 in dom (T | (B \ A)) and
A4: x2 in dom (T | (B \ A)) and
A5: (T | (B \ A)) . x1 = (T | (B \ A)) . x2 and
A6: x1 <> x2 ; :: thesis: contradiction
reconsider x2 = x2 as Element of V by A4;
reconsider x1 = x1 as Element of V by A3;
A7: dom T = [#] V by Th7;
then A8: x1 in B \ A by A3, RELAT_1:91;
A9: not x1 in A9 \/ {x2}

proof

assume A10: x1 in A9 \/ {x2} ; :: thesis: contradiction

per cases ( x1 in A9 or x1 in {x2} ) by A10, XBOOLE_0:def 3;

suppose x1 in A9 ; :: thesis: contradiction

hence contradiction by A8, XBOOLE_0:def 5; :: thesis: verum

end;

suppose x1 in {x2} ; :: thesis: contradiction

hence contradiction by A6, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A11: x2 in B \ A by A4, A7, RELAT_1:91;
then A12: (T | (B \ A)) . x2 = T . x2 by FUNCT_1:72;
reconsider A = A as Basis of ker T by A1;
A13: ker T = Lin A by VECTSP_7:def 3;
(T | (B \ A)) . x1 = T . x1 by A8, FUNCT_1:72;
then x1 - x2 in ker T by A5, A12, Th17;
then x1 - x2 in Lin A9 by A13, VECTSP_9:21;
then A14: x1 in Lin (A9 \/ {x2}) by Th18;
{x2} \/ {x1} = {x1,x2} by ENUMSET1:41;
then A15: (A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2} by XBOOLE_1:4;
{x1,x2} c= B

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x1,x2} or z in B )
assume A16: z in {x1,x2} ; :: thesis: z in B

per cases ( z = x1 or z = x2 ) by A16, TARSKI:def 2;

suppose z = x1 ; :: thesis: z in B

hence z in B by A8, XBOOLE_0:def 5; :: thesis: verum

end;

suppose z = x2 ; :: thesis: z in B

hence z in B by A11, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then A17: A9 \/ {x1,x2} c= B by A2, XBOOLE_1:8;
B is linearly-independent by VECTSP_7:def 3;
hence contradiction by A14, A15, A9, A17, Th21, VECTSP_7:2; :: thesis: verum