theorem :: RLVECT_4:10

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