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 & {v,w} is linearly-independent ) and
A2: 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
A3: ((a * u) + (b * v)) + (c * w) = 0. V and
A4: ( a <> 0 or b <> 0 or c <> 0 ) by A2, Th10;

now

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

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

(a * u) + ((b * v) + (c * w)) = 0. V by A3, RLVECT_1:def 3;
then a * u = - ((b * v) + (c * w)) by RLVECT_1:6;
then ((a ") * a) * u = (a ") * (- ((b * v) + (c * w))) by RLVECT_1:def 7;
then 1 * u = (a ") * (- ((b * v) + (c * w))) by A5, XCMPLX_0:def 7;
then u = (a ") * (- ((b * v) + (c * w))) by RLVECT_1:def 8
.= (a ") * ((- 1) * ((b * v) + (c * w))) by RLVECT_1:16
.= ((a ") * (- 1)) * ((b * v) + (c * w)) by RLVECT_1:def 7
.= (((a ") * (- 1)) * (b * v)) + (((a ") * (- 1)) * (c * w)) by RLVECT_1:def 5
.= ((((a ") * (- 1)) * b) * v) + (((a ") * (- 1)) * (c * w)) by RLVECT_1:def 7
.= ((((a ") * (- 1)) * b) * v) + ((((a ") * (- 1)) * c) * w) by RLVECT_1:def 7 ;
hence ex a, b being Real st u = (a * v) + (b * w) ; :: thesis: verum

end;

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

then 0. V = ((0. V) + (b * v)) + (c * w) by A3, RLVECT_1:10
.= (b * v) + (c * w) by RLVECT_1:4 ;
hence ex a, b being Real st u = (a * v) + (b * w) by A1, A4, A6, RLVECT_3:13; :: thesis: verum

end;

end;

end;

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