theorem :: RLVECT_X:18

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