let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(v - u)} is linearly-independent
let u, v be VECTOR of V; :: thesis: ( {u,v} is linearly-independent & u <> v implies {u,(v - u)} is linearly-independent )
assume A1: ( {u,v} is linearly-independent & u <> v ) ; :: thesis: {u,(v - u)} is linearly-independent
now :: thesis: for a, b being Real st (a * u) + (b * (v - u)) = 0. V holds
( a = 0 & b = 0 )
let a, b be Real; :: thesis: ( (a * u) + (b * (v - u)) = 0. V implies ( a = 0 & b = 0 ) )
assume (a * u) + (b * (v - u)) = 0. V ; :: thesis: ( a = 0 & b = 0 )
then A2: 0. V = (a * u) + ((b * v) - (b * u)) by RLVECT_1:34
.= ((a * u) + (b * v)) - (b * u) by RLVECT_1:def 3
.= ((a * u) - (b * u)) + (b * v) by RLVECT_1:def 3
.= ((a - b) * u) + (b * v) by RLVECT_1:35 ;
then a - b = 0 by A1, RLVECT_3:13;
hence ( a = 0 & b = 0 ) by A1, A2, RLVECT_3:13; :: thesis: verum
end;
hence {u,(v - u)} is linearly-independent by RLVECT_3:13; :: thesis: verum