theorem Th18: :: VECTSP_9:18

for GF being Field
for V being VectSp of GF
for A, B being finite Subset of V
for v being Vector of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being Vector of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )