theorem Th31: :: RLVECT_4:31

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