Positively oriented bases of an oriented vector space are path-connected

(Reduction to matrices.) Fix a positively oriented basis $b_0$ of $V$. By [F1] the map $A\mapsto A(b_0)$ is a bijection ${\mathrm{G}\mathrm{L}}^{+}(V)\to \{\text{positive bases}\}$ whose inverse sends a basis to its coordinate matrix; a family $t\mapsto b(t)$ of bases is continuous exactly when its matrix entries in $b_0$ are continuous. Choosing coordinates in $b_0$ identifies ${\mathrm{G}\mathrm{L}}^{+}(V)$ with ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$, so it suffices to prove that ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$ is path-connected.

(Deforming a factorisation to a diagonal sign matrix.) Let $A\in {\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$ and, by [F2], write $A=E_1\cdots E_m$ with each $E_i$ elementary. Replace each factor by a continuous path $E_i(t)$, $t\in [0,1]$, of invertible matrices with $E_i(0)=E_i$: for $E_i=T_{pq}(c)$ use $T_{pq}((1-t)c)$, for $E_i=D_p(c)$ with $c>0$ use $D_p((1-t)c+t)$, for $E_i=D_p(c)$ with $c<0$ use $D_p((1-t)c-t)$, and for $E_i=S_{pq}$ use $R_{pq}(1-t)D_q(-1)$, which starts at $S_{pq}$ by [F3] and ends at $D_q(-1)$; the endpoint $E_i(1)$ is $I$, $I$, $D_p(-1)$ or $D_q(-1)$ respectively, all diagonal with entries $\pm 1$. Every $E_i(t)$ is invertible: a transvection has determinant one, the scaling paths have a diagonal entry that is a convex combination of the two nonzero numbers $c$ and $1$ (respectively $c$ and $-1$) and so never vanishes, and the fourth path is a product of invertible matrices. Define $A(t):=E_1(t)\cdots E_m(t)$. Then $A(t)$ is invertible for every $t$, $A(0)=A$, and $A(1)=\mathrm{\Delta }$ is a product of matrices each of which is $I$ or some $D_p(-1)$, hence a diagonal matrix with entries $\pm 1$. Since $t\mapsto \det A(t)$ is continuous, never zero by invertibility, and positive at $t=0$, [F4] gives $\det A(t)>0$ for all $t$: so $A$ is joined to $\mathrm{\Delta }$ by a path in ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$.

(From the diagonal sign matrix to the identity.) The diagonal matrix $\mathrm{\Delta }$ has $\det \mathrm{\Delta }=\det A(1)>0$, so the number of its entries equal to $-1$ is even. Pair the indices $p<q$ carrying $-1$; for each pair, the matrix that is $-1$ on $\mathrm{span}\{e_p,e_q\}$ and $+1$ elsewhere is realised by the block $\left(\begin{array}{cc}\cos (\pi (1-t))& -\sin (\pi (1-t))\\ \sin (\pi (1-t))& \cos (\pi (1-t))\end{array}\right)$ at parameter $t$, which equals $-I_2$ on that plane at $t=0$, the identity at $t=1$, and has determinant $1$ throughout by [F3]. Doing this independently on the finitely many disjoint pairs and leaving the remaining coordinates fixed gives a continuous path $\mathrm{\Delta }(t)$ of invertible matrices with $\mathrm{\Delta }(0)=\mathrm{\Delta }$, $\mathrm{\Delta }(1)=I$. Because $\mathrm{\Delta }(t)$ is orthogonal of determinant $1$, this path lies in ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$; concatenating it with the smooth path of step 2.1 by the smooth reparametrisation of [F6] yields a smooth path in ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$ from $A$ to $I$.

(Conclusion.) Every $A\in {\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$ is joined to $I$ by a smooth path, and reversing paths joins any two elements of ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$ smoothly; hence ${\mathrm{G}\mathrm{L}}^{+}(k,\mathbb{R})$ is smoothly path-connected. By step 1.1 the set of positively oriented bases of $V$ is connected by smooth paths of positive bases; applied to the oriented vector space $T_y{S}^k$ it gives the asserted smooth path of positive bases at $y$. The case $k=0$ is the one-point space ${\mathrm{G}\mathrm{L}}^{+}(0,\mathbb{R})=\{I_0\}$. Every ingredient is an explicit formula, and the factorisation is a fixed finite one produced by the elimination theorem, so no choice principle is used.