for K being Field
for V being VectSp of K
for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U & v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U