theorem :: RLVECT_4:9

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