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