let a be 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
let V be 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
let u, v, w be VECTOR of V; ( {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
; {u,w,(a * v)} is linearly-independent
hence
{u,w,(a * v)} is linearly-independent
by Th7; verum