let a, b be Real; :: thesis: for V being RealLinearSpace
for v, w being VECTOR of V st a <> b holds
{(a * v),(b * v),w} is linearly-dependent
let V be RealLinearSpace; :: thesis: for v, w being VECTOR of V st a <> b holds
{(a * v),(b * v),w} is linearly-dependent
let v, w be VECTOR of V; :: thesis: ( a <> b implies {(a * v),(b * v),w} is linearly-dependent )
assume a <> b ; :: thesis: {(a * v),(b * v),w} is linearly-dependent
then {(a * v),(b * v)} is linearly-dependent by Th21;
hence {(a * v),(b * v),w} is linearly-dependent by RLVECT_3:5, SETWISEO:2; :: thesis: verum