Every Topological Vector Space is Regular

This is a version of the proof redrawn from topological groups:

$f(x,y) = x - y$ is continues function.

Without loss of generality we may assume that $x = 0$.

Then, if $U \in \mathcal{U}_V(Y) $, then where must exist two open sets $O$ and $O'$ such that $ Y \times \{ 0\} \subset O' \times O \subset f^{-1}$(U) as $y - 0 = y$ for all $y \in Y$.

Now we show that $ A =O' \cap (V \setminus U) + O = \emptyset$.

For every $y \in A$, there is a representation $y = v +z$ for some $z \not \in U$ and $v\in O$ . We also know that $y \in O'$. This means that $y - v \in U$ but we also know that $y - v = z \not \in U$, a contradiction. This shows that $A = \emptyset$

If $U$ was constructed as in the question above, then $O \subset (V\setminus U) + O$ as $0 \not \in U$ . Thus, $O \cap O' = \emptyset$

$\square$

This answer was written in order to close the question as it was essentially answered in the comments.