let F be Field; :: thesis: for V, W 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 V, W 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: (T " {(T . v)}) \ {v} misses A
proof
dom T = [#] V by Th7;
then A4: dom (T | A) = A by RELAT_1:62;
assume (T " {(T . v)}) \ {v} meets A ; :: thesis: contradiction
then consider x being object such that
A5: x in (T " {(T . v)}) \ {v} and
A6: x in A by XBOOLE_0:3;
not x in {v} by A5, XBOOLE_0:def 5;
then A7: x <> v by TARSKI:def 1;
x in T " {(T . v)} by A5, XBOOLE_0:def 5;
then T . x in {(T . v)} by FUNCT_1:def 7;
then A8: T . x = T . v by TARSKI:def 1;
T . x = (T | A) . x by A6, FUNCT_1:49;
then (T | A) . v = (T | A) . x by A2, A8, FUNCT_1:49;
hence contradiction by A1, A2, A6, A7, A4; :: thesis: verum
end;
take (T " {(T . v)}) \ {v} ; :: thesis: ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
{v} c= T " {(T . v)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in T " {(T . v)} )
assume x in {v} ; :: thesis: x in T " {(T . v)}
then A9: x = v by TARSKI:def 1;
( dom T = [#] V & T . v in {(T . v)} ) by Th7, TARSKI:def 1;
hence x in T " {(T . v)} by A9, FUNCT_1:def 7; :: thesis: verum
end;
hence ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) ) by A3, XBOOLE_1:45; :: thesis: verum