let a be Real; for V being RealLinearSpace
for v, w being VECTOR of V st a <> 1 holds
{v,(a * v),w} is linearly-dependent
let V be RealLinearSpace; for v, w being VECTOR of V st a <> 1 holds
{v,(a * v),w} is linearly-dependent
let v, w be VECTOR of V; ( a <> 1 implies {v,(a * v),w} is linearly-dependent )
v = 1 * v
by RLVECT_1:def 8;
hence
( a <> 1 implies {v,(a * v),w} is linearly-dependent )
by Th31; verum