for V being RealLinearSpace
for v, w being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds
ex a being Real st v = a * w