[proofplan] The strategy is to exhibit the identity $g_*([\gamma]) = u_\#(f_*([\gamma]))$ for an arbitrary loop $\gamma$ at $x_0$ by building a homotopy of loops in $Y$ that uses the full two-parameter data of the ambient homotopy $H$. We form the composite $F := H \circ (\gamma \times \operatorname{id}_I): I \times I \to Y$, which records the whole deformation of $\gamma$ along $H$. We then choose two paths $\ell^+, \ell^-: I \to I \times I$ in the square — the top edge, and the bottom edge bracketed by the two vertical edges — whose images under $F$ compute $g \circ \gamma$ and $u^{-1} \cdot (f \circ \gamma) \cdot u$ respectively. Because $I \times I$ is convex, the straight-line homotopy between $\ell^+$ and $\ell^-$ (relative endpoints) pushes forward under $F$ to a based-loop homotopy in $Y$ between $g \circ \gamma$ and $u^{-1} \cdot (f \circ \gamma) \cdot u$, yielding the desired identity after passing to $\pi_1$. [/proofplan]

[step:Fix a loop $\gamma$ and reduce to a based-homotopy statement in $Y$] Let $[\gamma] \in \pi_1(X, x_0)$ and choose a representative loop \begin{align*} \gamma: I &\to X \\ s &\mapsto \gamma(s) \end{align*} with $\gamma(0) = \gamma(1) = x_0$. By the definitions of the induced map on $\pi_1$ and of the [change-of-basepoint isomorphism](/theorems/???) $u_\#$, \begin{align*} f_*([\gamma]) &= [f \circ \gamma] \in \pi_1(Y, f(x_0)), \\ g_*([\gamma]) &= [g \circ \gamma] \in \pi_1(Y, g(x_0)), \\ u_\#([f \circ \gamma]) &= [u^{-1} \cdot (f \circ \gamma) \cdot u] \in \pi_1(Y, g(x_0)). \end{align*} The identity $g_* = u_\# \circ f_*$ at the class $[\gamma]$ is therefore equivalent to the based-homotopy statement \begin{align*} g \circ \gamma \simeq u^{-1} \cdot (f \circ \gamma) \cdot u \qquad \text{rel } \{0, 1\} \text{ in } Y, \end{align*} where both sides are loops at $g(x_0)$ (the right-hand side lands at $g(x_0)$ because $u$ starts at $f(x_0)$ and ends at $g(x_0)$, so $u^{-1}$ starts at $g(x_0)$ and the concatenation returns to $g(x_0)$). The remainder of the proof constructs such a based homotopy. [/step]

[step:Build the auxiliary map $F: I \times I \to Y$ by pulling back $H$ along $\gamma$]Define the continuous map \begin{align*} F: I \times I &\to Y \\ (s, t) &\mapsto H(\gamma(s), t). \end{align*} Equivalently, $F = H \circ (\gamma \times \operatorname{id}_I)$, which is continuous as a composition of continuous maps. The square $I \times I$ is our parameter space for loop-and-time, with $s$ indexing position along the loop and $t$ indexing the homotopy parameter. We record the boundary values of $F$ once and for all, since every subsequent computation reduces to these: \begin{align*} F(s, 0) &= H(\gamma(s), 0) = f(\gamma(s)) &&\text{(bottom edge)}, \\ F(s, 1) &= H(\gamma(s), 1) = g(\gamma(s)) &&\text{(top edge)}, \\ F(0, t) &= H(\gamma(0), t) = H(x_0, t) = u(t) &&\text{(left edge)}, \\ F(1, t) &= H(\gamma(1), t) = H(x_0, t) = u(t) &&\text{(right edge)}, \end{align*} using $\gamma(0) = \gamma(1) = x_0$ and the definition $u(t) = H(x_0, t)$.[/step]

[guided]We want to prove the based-loop homotopy $g \circ \gamma \simeq u^{-1} \cdot (f \circ \gamma) \cdot u$. The obstruction is that the homotopy $H$ does not fix the basepoint $x_0$: as $t$ varies, $H(x_0, t)$ traces the path $u$. So any attempt to directly homotope $g \circ \gamma$ to $f \circ \gamma$ via the formula $(s, t) \mapsto H(\gamma(s), 1 - t)$ produces an endpoint-moving homotopy, not a based one. The path $u$ and its reverse $u^{-1}$ are the "correction" that compensates for this endpoint drift. The map $F(s, t) = H(\gamma(s), t)$ packages all the available data. To read a based loop out of $F$, we read the image of some path in $I \times I$. The four edges of the square give: - the bottom ($t = 0$): the loop $f \circ \gamma$, based at $f(x_0)$; - the top ($t = 1$): the loop $g \circ \gamma$, based at $g(x_0)$; - the left ($s = 0$) and right ($s = 1$) vertical edges: both traverse $u$, from $f(x_0)$ to $g(x_0)$. This four-edge picture is the bookkeeping for the proof: the top edge alone gives $g \circ \gamma$; the left–bottom–right boundary (traversed counterclockwise from the top-left corner) gives $u^{-1} \cdot (f \circ \gamma) \cdot u$. The two edge paths share endpoints, namely the top-left and top-right corners of the square, both of which $F$ sends to $g(x_0)$. So if we can homotope the two edge paths in $I \times I$ rel endpoints, pushing forward by $F$ will give the based-loop homotopy we need.[/guided]

[step:Exhibit two paths $\ell^+, \ell^-: I \to I \times I$ whose $F$-images are the two sides of the desired identity] Define the top-edge path \begin{align*} \ell^+: I &\to I \times I \\ s &\mapsto (s, 1). \end{align*} Define the three-sided path $\ell^-: I \to I \times I$ by traversing, in order, the left edge downward, the bottom edge rightward, and the right edge upward. Using the standard reparametrisation of the interval into thirds, set \begin{align*} \ell^-(s) = \begin{cases} (0, \, 1 - 3s) & \text{if } s \in [0, 1/3], \\ (3s - 1, \, 0) & \text{if } s \in [1/3, 2/3], \\ (1, \, 3s - 2) & \text{if } s \in [2/3, 1]. \end{cases} \end{align*} The three pieces agree at the junction points $s = 1/3$ (both give $(0, 0)$) and $s = 2/3$ (both give $(1, 0)$), so $\ell^-$ is continuous. Its endpoints are $\ell^-(0) = (0, 1)$ and $\ell^-(1) = (1, 1)$, matching those of $\ell^+$. We compute $F \circ \ell^+$ and $F \circ \ell^-$ using the boundary values recorded in the previous step. First, \begin{align*} (F \circ \ell^+)(s) = F(s, 1) = g(\gamma(s)) = (g \circ \gamma)(s). \end{align*} Second, on the three subintervals, \begin{align*} s \in [0, 1/3]: \quad (F \circ \ell^-)(s) &= F(0, 1 - 3s) = u(1 - 3s), \\ s \in [1/3, 2/3]: \quad (F \circ \ell^-)(s) &= F(3s - 1, 0) = f(\gamma(3s - 1)), \\ s \in [2/3, 1]: \quad (F \circ \ell^-)(s) &= F(1, 3s - 2) = u(3s - 2). \end{align*} On $[0, 1/3]$, $s \mapsto u(1 - 3s)$ is the standard third-interval reparametrisation of the reversed path $u^{-1}(t) := u(1 - t)$; on $[1/3, 2/3]$ we see the standard reparametrisation of $f \circ \gamma$; on $[2/3, 1]$ the standard reparametrisation of $u$. By the definition of path concatenation, \begin{align*} F \circ \ell^- = u^{-1} \cdot (f \circ \gamma) \cdot u. \end{align*} [/step]

[step:Homotope $\ell^+$ to $\ell^-$ in $I \times I$ by the straight-line homotopy rel endpoints]The square $I \times I \subseteq \mathbb{R}^2$ is convex, so for any two paths with common endpoints the straight-line homotopy lies in $I \times I$. Define \begin{align*} L: I \times I &\to I \times I \\ (s, t) &\mapsto (1 - t)\, \ell^+(s) + t\, \ell^-(s). \end{align*} This is continuous; its image lies in $I \times I$ by convexity; and it satisfies \begin{align*} L(s, 0) &= \ell^+(s), & L(s, 1) &= \ell^-(s), \\ L(0, t) &= (1 - t)(0, 1) + t(0, 1) = (0, 1), & L(1, t) &= (1 - t)(1, 1) + t(1, 1) = (1, 1), \end{align*} the last two lines using $\ell^+(0) = \ell^-(0) = (0, 1)$ and $\ell^+(1) = \ell^-(1) = (1, 1)$. Hence $L$ is a homotopy $\ell^+ \simeq \ell^-$ rel $\{0, 1\}$ in $I \times I$.[/step]

[guided]Why does the straight-line homotopy work here and not in general? The obstruction to using the straight-line formula $(1 - t) \alpha(s) + t \beta(s)$ between two paths $\alpha$ and $\beta$ is that the intermediate values might leave the ambient space. Here the ambient space is the square $I \times I$, a convex subset of $\mathbb{R}^2$, so every convex combination of points of $I \times I$ remains in $I \times I$. Convexity is exactly the hypothesis that makes the formula well-defined as a map into $I \times I$. The "rel endpoints" property follows because $\ell^+$ and $\ell^-$ agree at $s = 0$ and $s = 1$: at those values the convex combination is constant in $t$. This will be crucial in the next step: we want a based-loop homotopy in $Y$, and pushing $L$ forward by $F$ will keep the endpoints $F(0, 1) = g(x_0)$ and $F(1, 1) = g(x_0)$ fixed throughout precisely because $L$ is stationary at $s = 0$ and $s = 1$.[/guided]

[step:Push $L$ forward by $F$ to obtain the based-loop homotopy in $Y$] Define \begin{align*} K: I \times I &\to Y \\ (s, t) &\mapsto F(L(s, t)). \end{align*} This is continuous as the composition of continuous maps. Its boundary behaviour follows from that of $L$: \begin{align*} K(s, 0) &= F(\ell^+(s)) = (g \circ \gamma)(s), \\ K(s, 1) &= F(\ell^-(s)) = \bigl(u^{-1} \cdot (f \circ \gamma) \cdot u\bigr)(s), \\ K(0, t) &= F(0, 1) = H(x_0, 1) = g(x_0), \\ K(1, t) &= F(1, 1) = H(x_0, 1) = g(x_0), \end{align*} using $L(0, t) = (0, 1)$ and $L(1, t) = (1, 1)$. Thus $K$ is a homotopy \begin{align*} g \circ \gamma \; \simeq \; u^{-1} \cdot (f \circ \gamma) \cdot u \qquad \text{rel } \{0, 1\} \end{align*} of loops based at $g(x_0)$ in $Y$. Passing to $\pi_1(Y, g(x_0))$, \begin{align*} g_*([\gamma]) = [g \circ \gamma] = [u^{-1} \cdot (f \circ \gamma) \cdot u] = u_\#([f \circ \gamma]) = u_\#(f_*([\gamma])). \end{align*} Since $[\gamma] \in \pi_1(X, x_0)$ was arbitrary, $g_* = u_\# \circ f_*$ as maps $\pi_1(X, x_0) \to \pi_1(Y, g(x_0))$, which is the claim. [/step]

<!-- illustration-needed: the unit square I x I with the two paths ell-plus (top edge from (0,1) to (1,1)) and ell-minus (left edge from (0,1) down to (0,0), bottom edge to (1,0), right edge up to (1,1)) drawn and labelled; the straight-line homotopy L indicated by a few intermediate paths sweeping from top to the U-shape; the four edges labelled with their F-images: top = g o gamma, bottom = f o gamma, left = u, right = u -->