theorem :: RLVECT_4:16

for x being set
for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )