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