for X being LinearTopSpace
for x being Point of X
for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x