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