let a be Real; :: thesis: for V being RealLinearSpace
for u, w, v 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
let V be RealLinearSpace; :: thesis: for u, w, v 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
let u, w, v be VECTOR of V; :: thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 implies {u,w,(a * v)} is linearly-independent )
assume that
A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) and
A2: a <> 0 ; :: thesis: {u,w,(a * v)} is linearly-independent

now

let b, c, d be Real; :: thesis: ( ((b * u) + (c * w)) + (d * (a * v)) = 0. V implies ( b = 0 & c = 0 & d = 0 ) )
assume ((b * u) + (c * w)) + (d * (a * v)) = 0. V ; :: thesis: ( b = 0 & c = 0 & d = 0 )
then A3: 0. V = ((b * u) + (c * w)) + ((d * a) * v) by RLVECT_1:def 10;
then d * a = 0 by A1, Th10;
hence ( b = 0 & c = 0 & d = 0 ) by A1, A2, A3, Th10, XCMPLX_1:6; :: thesis: verum

end;

hence {u,w,(a * v)} is linearly-independent by Th10; :: thesis: verum