theorem :: RLVECT_4:36

for V being RealLinearSpace
for u, v, w being VECTOR of V st v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent holds
ex a, b being Real st u = (a * v) + (b * w)