let W be Z_Module; :: thesis: for V being free finite-rank Z_Module
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let V be free finite-rank Z_Module; :: thesis: for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W 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
for T being linear-transformation of V,W 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: for T being linear-transformation of V,W 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: ( 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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (T | (B \ A)) or not x2 in dom (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
x2 in dom T by A4, RELAT_1:57;
then reconsider x2 = x2 as Element of V ;
x1 in dom T by A3, RELAT_1:57;
then reconsider x1 = x1 as Element of V ;
A7: not x1 in A9 \/ {x2}

proof

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

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

suppose x1 in A9 ; :: thesis: contradiction

hence contradiction by A3, 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;

A9: (T | (B \ A)) . x2 = T . x2 by A4, FUNCT_1:49;
reconsider A = A as Subset of (ker T) by A1;
reconsider A = A as Basis of (ker T) by A1;
A10: ker T = Lin A by VECTSP_7:def 3;
(T | (B \ A)) . x1 = T . x1 by A3, FUNCT_1:49;
then x1 - x2 in ker T by A5, A9, Th17;
then x1 - x2 in Lin A9 by A10, ZMODUL03:20;
then A11: x1 in Lin (A9 \/ {x2}) by Th18;
{x2} \/ {x1} = {x1,x2} by ENUMSET1:1;
then A12: (A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2} by XBOOLE_1:4;
{x1,x2} c= B

proof

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

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

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

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

end;

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

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

end;

end;

end;

then A14: A9 \/ {x1,x2} c= B by A2, XBOOLE_1:8;
B is linearly-independent by VECTSP_7:def 3;
hence contradiction by A7, A11, A12, A14, Th21, ZMODUL02:56; :: thesis: verum