Membership in the Line ℝx₀ of a Real Vector Space

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Real Normed, Inner Product and Hilbert Spaces: Notation, let $V$ be a real vector space.

(i) Let $x_{0}\in V$, and let $\mathbb{R}x_{0}=\{y:\text{there is }t\in\mathbb{R}\text{ with }y=tx_{0}\}$, a class abstraction. For every class $y$, $y\in\mathbb{R}x_{0}$ if and only if there is $t\in\mathbb{R}$ with $y=tx_{0}$.