theorem Th27: :: RLVECT_4:27

for a being Real
for V being RealLinearSpace
for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds
{u,w,(a * v)} is linearly-independent