for x being set
for V being RealLinearSpace
for v being VECTOR of V holds
( x in Z_Lin {v} iff ex a being Integer st x = a * v )