let V be RealLinearSpace; :: thesis: for v, w, u being VECTOR of V st v <> w & {v,w} is linearly-independent & not {u,v,w} is linearly-independent holds
ex a, b being Real st u = (a * v) + (b * w)
let v, w, u be VECTOR of V; :: thesis: ( v <> w & {v,w} is linearly-independent & not {u,v,w} is linearly-independent implies ex a, b being Real st u = (a * v) + (b * w) )
assume that
A1: v <> w and
A2: {v,w} is linearly-independent and
A3: not {u,v,w} is linearly-independent ; :: thesis: ex a, b being Real st u = (a * v) + (b * w)
consider a, b, c being Real such that
A4: ((a * u) + (b * v)) + (c * w) = 0. V and
A5: ( a <> 0 or b <> 0 or c <> 0 ) by A3, Th10;

now

per cases ( a <> 0 or a = 0 ) ;

suppose A6: a <> 0 ; :: thesis: ex a, b being Real st u = (a * v) + (b * w)

(a * u) + ((b * v) + (c * w)) = 0. V by A4, RLVECT_1:def 6;
then a * u = - ((b * v) + (c * w)) by RLVECT_1:19;
then ((a " ) * a) * u = (a " ) * (- ((b * v) + (c * w))) by RLVECT_1:def 9;
then 1 * u = (a " ) * (- ((b * v) + (c * w))) by A6, XCMPLX_0:def 7;
then u = (a " ) * (- ((b * v) + (c * w))) by RLVECT_1:def 9
.= (a " ) * ((- 1) * ((b * v) + (c * w))) by RLVECT_1:29
.= ((a " ) * (- 1)) * ((b * v) + (c * w)) by RLVECT_1:def 9
.= (((a " ) * (- 1)) * (b * v)) + (((a " ) * (- 1)) * (c * w)) by RLVECT_1:def 9
.= ((((a " ) * (- 1)) * b) * v) + (((a " ) * (- 1)) * (c * w)) by RLVECT_1:def 9
.= ((((a " ) * (- 1)) * b) * v) + ((((a " ) * (- 1)) * c) * w) by RLVECT_1:def 9 ;
hence ex a, b being Real st u = (a * v) + (b * w) ; :: thesis: verum

end;

suppose A7: a = 0 ; :: thesis: ex a, b being Real st u = (a * v) + (b * w)

then 0. V = ((0. V) + (b * v)) + (c * w) by A4, RLVECT_1:23
.= (b * v) + (c * w) by RLVECT_1:10 ;
hence ex a, b being Real st u = (a * v) + (b * w) by A1, A2, A5, A7, RLVECT_3:14; :: thesis: verum

end;

end;

end;

hence ex a, b being Real st u = (a * v) + (b * w) ; :: thesis: verum