Loops in $\mathbb R^m\setminus\{0\}$, $m\ge3$, are null-homotopic rel base point

Let $\iota$ be a finite set with at least three elements and let $x_0\in\mathbb R^\iota$. If $v:[0,1]\to\mathbb R^\iota\setminus\{0\}$ is continuous with $v(0)=v(1)=x_0$, then there is a continuous map $H:[0,1]\times[0,1]\to\mathbb R^\iota\setminus\{0\}$ with

That is, $\mathbb R^m\setminus\{0\}$ is simply connected for $m\ge3$, stated in the concrete form of a based null-homotopy of an arbitrary based loop. It is used for loops of vectors $t\mapsto\varphi(t)v_0$ obtained from loops $\varphi$ of matrices.

Formalization Note. $\mathbb R^\iota$ is the function space ι → ℝ with its product topology, for [Fintype ι] with 3 ≤ Fintype.card ι; the loop and the homotopy are C(unitInterval, ι → ℝ) and C(unitInterval × unitInterval, ι → ℝ), and the condition $H\neq0$ is required at every point.