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 l being Linear_Combination of A
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let W, V be VectSp of F; :: thesis: for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let T be linear-transformation of V,W; :: thesis: for A being Subset of V
for l being Linear_Combination of A
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let A be Subset of V; :: thesis: for l being Linear_Combination of A
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let l be Linear_Combination of A; :: thesis: for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let v be Element of V; :: thesis: ( T | A is one-to-one & v in A implies ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X ) )
assume that
A1: T | A is one-to-one and
A2: v in A ; :: thesis: ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
set X = (T " {(T . v)}) \ {v};
A3: {v} c= T " {(T . v)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in T " {(T . v)} )
assume A4: x in {v} ; :: thesis: x in T " {(T . v)}
A5: x = v by A4, TARSKI:def 1;
A6: dom T = [#] V by Th7;
T . v in {(T . v)} by TARSKI:def 1;
hence x in T " {(T . v)} by A5, A6, FUNCT_1:def 13; :: thesis: verum

end;

A7: (T " {(T . v)}) \ {v} misses A

proof

assume (T " {(T . v)}) \ {v} meets A ; :: thesis: contradiction
then consider x being set such that
A8: x in (T " {(T . v)}) \ {v} and
A9: x in A by XBOOLE_0:3;
A10: x in T " {(T . v)} by A8, XBOOLE_0:def 5;
not x in {v} by A8, XBOOLE_0:def 5;
then A11: x <> v by TARSKI:def 1;
T . x in {(T . v)} by A10, FUNCT_1:def 13;
then A12: T . x = T . v by TARSKI:def 1;
T . x = (T | A) . x by A9, FUNCT_1:72;
then A13: (T | A) . v = (T | A) . x by A2, A12, FUNCT_1:72;
dom T = [#] V by Th7;
then dom (T | A) = A by RELAT_1:91;
hence contradiction by A1, A2, A9, A11, A13, FUNCT_1:def 8; :: thesis: verum

end;

take (T " {(T . v)}) \ {v} ; :: thesis: ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
thus ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) ) by A3, A7, XBOOLE_1:45; :: thesis: verum