let F be Field; :: thesis: for V being VectSp of
for A, B being finite Subset of st B c= A holds
for v being Vector of st v in Lin A & not v in Lin B holds
ex w being Vector of st
( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )
let V be VectSp of ; :: thesis: for A, B being finite Subset of st B c= A holds
for v being Vector of st v in Lin A & not v in Lin B holds
ex w being Vector of st
( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )
let A, B be finite Subset of ; :: thesis: ( B c= A implies for v being Vector of st v in Lin A & not v in Lin B holds
ex w being Vector of st
( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) )
assume B c= A ; :: thesis: for v being Vector of st v in Lin A & not v in Lin B holds
ex w being Vector of 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 st v in Lin A & not v in Lin B holds
ex w being Vector of st
( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) by VECTSP_9:22; :: thesis: verum