let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(- v)} is linearly-independent
let u, v be VECTOR of V; :: thesis: ( {u,v} is linearly-independent & u <> v implies {u,(- v)} is linearly-independent )
assume A1: ( {u,v} is linearly-independent & u <> v ) ; :: thesis: {u,(- v)} is linearly-independent
( - 1 <> 0 & - v = (- 1) * v ) by RLVECT_1:29;
hence {u,(- v)} is linearly-independent by A1, Th22; :: thesis: verum