let a, b be Real; :: thesis: for V being RealLinearSpace
for v being VECTOR of V st a <> b holds
not {(a * v),(b * v)} is linearly-independent
let V be RealLinearSpace; :: thesis: for v being VECTOR of V st a <> b holds
not {(a * v),(b * v)} is linearly-independent
let v be VECTOR of V; :: thesis: ( a <> b implies not {(a * v),(b * v)} is linearly-independent )
assume A1: a <> b ; :: thesis: not {(a * v),(b * v)} is linearly-independent

now

per cases ( v = 0. V or v <> 0. V ) ;

suppose v = 0. V ; :: thesis: not {(a * v),(b * v)} is linearly-independent

then a * v = 0. V by RLVECT_1:23;
hence not {(a * v),(b * v)} is linearly-independent by RLVECT_3:12; :: thesis: verum

end;

suppose A2: v <> 0. V ; :: thesis: not {(a * v),(b * v)} is linearly-independent

A3: (b * (a * v)) + ((- a) * (b * v)) = ((a * b) * v) + ((- a) * (b * v)) by RLVECT_1:def 10
.= ((a * b) * v) - (a * (b * v)) by Th6
.= ((a * b) * v) - ((a * b) * v) by RLVECT_1:def 10
.= 0. V by RLVECT_1:28 ;
A4: ( not b = 0 or not - a = 0 ) by A1;
a * v <> b * v by A1, A2, RLVECT_1:51;
hence not {(a * v),(b * v)} is linearly-independent by A3, A4, RLVECT_3:14; :: thesis: verum

end;

end;

end;

hence not {(a * v),(b * v)} is linearly-independent ; :: thesis: verum