Proof of The Line t ↦ x+th and Values of a Function along a Line in ℝⁿ, as Functions

For (i): for every $t\in J$, $x+th$ is a point of $\mathbb{R}^{n}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv), and it is the only $v\in\mathbb{R}^{n}$ with $v=x+th$; so Maps from Functional Predicative Relations, and Families of Sections (ii), applied to the formula $v=x+th$ with parameters $x$ and $h$, gives a map $\gamma:J\to\mathbb{R}^{n}$ with $\gamma(t)=x+th$ for every $t\in J$.

For (ii): for every $t\in J$ we have $x+th\in U$, so $F(x+th)\in Y$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i); Maps from Functional Predicative Relations, and Families of Sections (ii), applied to the formula $v=F(x+th)$ with parameters $F$, $x$ and $h$, gives $\varphi:J\to Y$ with $\varphi(t)=F(x+th)$ for every $t\in J$.