theorem :: RLVECT_X:21

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