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 + u),(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 + u),(v + u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; :: thesis: {u,(w + u),(v + u)} is linearly-independent

now :: thesis: for a, b, c being Real st ((a * u) + (b * (w + u))) + (c * (v + u)) = 0. V holds
( a = 0 & b = 0 & c = 0 )

let a, b, c be Real; :: thesis: ( ((a * u) + (b * (w + u))) + (c * (v + u)) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume ((a * u) + (b * (w + u))) + (c * (v + u)) = 0. V ; :: thesis: ( a = 0 & b = 0 & c = 0 )
then A2: 0. V = ((a * u) + ((b * u) + (b * w))) + (c * (v + u)) by RLVECT_1:def 5
.= (((a * u) + (b * u)) + (b * w)) + (c * (v + u)) by RLVECT_1:def 3
.= (((a + b) * u) + (b * w)) + (c * (v + u)) by RLVECT_1:def 6
.= (((a + b) * u) + (b * w)) + ((c * u) + (c * v)) by RLVECT_1:def 5
.= ((a + b) * u) + ((b * w) + ((c * u) + (c * v))) by RLVECT_1:def 3
.= ((a + b) * u) + ((c * u) + ((b * w) + (c * v))) by RLVECT_1:def 3
.= (((a + b) * u) + (c * u)) + ((b * w) + (c * v)) by RLVECT_1:def 3
.= (((a + b) + c) * u) + ((b * w) + (c * v)) by RLVECT_1:def 6
.= ((((a + b) + c) * u) + (b * w)) + (c * v) by RLVECT_1:def 3 ;
then ( (a + b) + c = 0 & b = 0 ) by A1, Th7;
hence ( a = 0 & b = 0 & c = 0 ) by A1, A2, Th7; :: thesis: verum

end;

hence {u,(w + u),(v + u)} is linearly-independent by Th7; :: thesis: verum