let F be Field; :: thesis: for V being VectSp of F

for A, B being finite Subset of V st B c= A holds

for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

let V be VectSp of F; :: thesis: for A, B being finite Subset of V st B c= A holds

for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

let A, B be finite Subset of V; :: thesis: ( B c= A implies for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) )

assume B c= A ; :: thesis: for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

then A = B \/ (A \ B) by XBOOLE_1:45;

hence for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) by VECTSP_9:18; :: thesis: verum

for A, B being finite Subset of V st B c= A holds

for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

let V be VectSp of F; :: thesis: for A, B being finite Subset of V st B c= A holds

for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

let A, B be finite Subset of V; :: thesis: ( B c= A implies for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) )

assume B c= A ; :: thesis: for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )

then A = B \/ (A \ B) by XBOOLE_1:45;

hence for v being Vector of V st v in Lin A & not v in Lin B holds

ex w being Vector of V st

( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) by VECTSP_9:18; :: thesis: verum