theorem :: RLVECT_X:17

for V being RealLinearSpace
for v being VECTOR of V holds v in Z_Lin {v}