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