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

now

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

suppose A6: a <> 0 ; :: thesis: ex a being Real st v = a * w

((a " ) * a) * v = (a " ) * (- (b * w)) by A5, RLVECT_1:def 9;
then 1 * v = (a " ) * (- (b * w)) by A6, XCMPLX_0:def 7;
then v = (a " ) * (- (b * w)) by RLVECT_1:def 9
.= (a " ) * ((- b) * w) by Th6
.= ((a " ) * (- b)) * w by RLVECT_1:def 9 ;
hence ex a being Real st v = a * w ; :: thesis: verum

end;

suppose a = 0 ; :: thesis: ex a being Real st v = a * w

then ( 0. V = - (b * w) & b <> 0 ) by A4, A5, RLVECT_1:23;
then ( 0. V = (- b) * w & - b <> 0 ) by Th6;
hence ex a being Real st v = a * w by A1, RLVECT_1:24; :: thesis: verum

end;

end;

end;

hence ex a being Real st v = a * w ; :: thesis: verum