theorem :: RLVECT_4:22

for a being Real
for V being RealLinearSpace
for v being VECTOR of V st a <> 1 holds
{v,(a * v)} is linearly-dependent