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