theorem Th21: :: RLVECT_4:21

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