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