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

{v} c= T " {(T . v)}

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

take
(T " {(T . v)}) \ {v}
; :: thesis: ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
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;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

{v} c= T " {(T . v)}

proof

hence
( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
by A3, XBOOLE_1:45; :: thesis: verum
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;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