[proofplan] We first verify that $[\gamma] \mapsto [f \circ \gamma]$ is well defined by transporting a path homotopy $H$ through $f$; the result $f \circ H$ is again a path homotopy because $f$ preserves the basepoint constraints. Next we check $f_*$ is a [group homomorphism](/pages/Group%20Homomorphism): the identity $f \circ (\gamma_0 \cdot \gamma_1) = (f \circ \gamma_0) \cdot (f \circ \gamma_1)$ holds pointwise from the piecewise formula for concatenation. The remaining properties — based homotopy invariance, the composition law, and identity preservation — descend from the corresponding properties established for $\pi_0$ in [Theorem 1875](/theorems/1875), with the additional verification that the homotopies remain rel-basepoint. [/proofplan]

[step:Verify that $f_*$ is well defined on path homotopy classes]Let $\gamma, \gamma': I \to X$ be loops at $x_0$ with $[\gamma] = [\gamma']$ in $\pi_1(X, x_0)$. Then $f \circ \gamma$ and $f \circ \gamma'$ are loops at $y_0 = f(x_0)$: each is a composition of continuous maps, and \begin{align*} (f \circ \gamma)(0) = f(\gamma(0)) = f(x_0) = y_0, \qquad (f \circ \gamma)(1) = f(\gamma(1)) = f(x_0) = y_0, \end{align*} and similarly for $\gamma'$. By hypothesis there exists a path homotopy $H: I \times I \to X$ with \begin{align*} H(s, 0) = \gamma(s), \quad H(s, 1) = \gamma'(s), \quad H(0, t) = H(1, t) = x_0 \text{ for all } t \in I. \end{align*} Define \begin{align*} K := f \circ H: I \times I &\to Y \\ (s, t) &\mapsto f(H(s, t)). \end{align*} Continuity of $K$ follows from the continuity of $H$ and $f$. At the boundary, \begin{align*} K(s, 0) = f(H(s, 0)) = f(\gamma(s)) = (f \circ \gamma)(s), \quad K(s, 1) = (f \circ \gamma')(s), \end{align*} and at the endpoints, \begin{align*} K(0, t) = f(H(0, t)) = f(x_0) = y_0, \quad K(1, t) = f(H(1, t)) = f(x_0) = y_0 \text{ for all } t \in I. \end{align*} Thus $K$ is a path homotopy from $f \circ \gamma$ to $f \circ \gamma'$ rel $\{0, 1\}$, so $[f \circ \gamma] = [f \circ \gamma']$ in $\pi_1(Y, y_0)$. The assignment $[\gamma] \mapsto [f \circ \gamma]$ therefore descends to a well-defined function \begin{align*} f_*: \pi_1(X, x_0) \to \pi_1(Y, y_0). \end{align*}[/step]

[guided]Two things need checking: that $f \circ \gamma$ is actually a loop at $y_0$ (otherwise the output class makes no sense), and that the output class is independent of the representative $\gamma$. For the first, composition of continuous maps is continuous, so $f \circ \gamma$ is continuous as a map $I \to Y$. The endpoints work out because $\gamma(0) = \gamma(1) = x_0$ and $f(x_0) = y_0$ by hypothesis (the map is based). So $f \circ \gamma$ really is a loop at $y_0$. For representative-independence, suppose $\gamma' $ is another loop at $x_0$ with $[\gamma] = [\gamma']$. This gives a path homotopy $H: I \times I \to X$ with $H|_{I \times \{0\}} = \gamma$, $H|_{I \times \{1\}} = \gamma'$, and $H(0, t) = H(1, t) = x_0$ for all $t$. We need a path homotopy in $Y$ from $f \circ \gamma$ to $f \circ \gamma'$. The obvious candidate is $K := f \circ H$. Continuity is free. The boundary conditions at $t = 0, 1$ are exactly what we want: \begin{align*} K(s, 0) = f(\gamma(s)) = (f \circ \gamma)(s), \qquad K(s, 1) = f(\gamma'(s)) = (f \circ \gamma')(s). \end{align*} The crucial check is the **rel-endpoints** condition. At $s = 0$: $H(0, t) = x_0$, so $K(0, t) = f(x_0) = y_0$, constant in $t$. At $s = 1$: same calculation. This is where we use that $f$ is **based** — we need $f$ to map the fixed basepoint $x_0$ to the fixed basepoint $y_0$, so that the homotopy remains rel the distinguished basepoint downstairs. **Why would this fail for an unbased map?** If $f$ did not map $x_0$ to $y_0$, then $K(0, t) = f(x_0)$ might not equal the chosen basepoint of $Y$, and $f \circ \gamma$ would not even be a loop at $y_0$ in the first place.[/guided]

[step:Verify $f_*$ is a group homomorphism]Let $\gamma_0, \gamma_1$ be loops at $x_0$. From the definition of [path concatenation](/pages/Path%20Concatenation), \begin{align*} (\gamma_0 \cdot \gamma_1)(s) = \begin{cases} \gamma_0(2s) & 0 \le s \le 1/2, \\ \gamma_1(2s - 1) & 1/2 \le s \le 1. \end{cases} \end{align*} Applying $f$ pointwise, \begin{align*} (f \circ (\gamma_0 \cdot \gamma_1))(s) = \begin{cases} f(\gamma_0(2s)) & 0 \le s \le 1/2, \\ f(\gamma_1(2s - 1)) & 1/2 \le s \le 1, \end{cases} = \begin{cases} (f \circ \gamma_0)(2s) & 0 \le s \le 1/2, \\ (f \circ \gamma_1)(2s - 1) & 1/2 \le s \le 1. \end{cases} \end{align*} The right-hand side is precisely $((f \circ \gamma_0) \cdot (f \circ \gamma_1))(s)$. Hence, as maps $I \to Y$, \begin{align*} f \circ (\gamma_0 \cdot \gamma_1) = (f \circ \gamma_0) \cdot (f \circ \gamma_1). \end{align*} Taking path homotopy classes, \begin{align*} f_*([\gamma_0] \cdot [\gamma_1]) &= f_*([\gamma_0 \cdot \gamma_1]) \qquad \text{(definition of the group law on } \pi_1) \\ &= [f \circ (\gamma_0 \cdot \gamma_1)] \qquad \text{(definition of } f_*) \\ &= [(f \circ \gamma_0) \cdot (f \circ \gamma_1)] \qquad \text{(pointwise equality above)} \\ &= [f \circ \gamma_0] \cdot [f \circ \gamma_1] \qquad \text{(definition of the group law on } \pi_1) \\ &= f_*([\gamma_0]) \cdot f_*([\gamma_1]). \end{align*} Thus $f_*$ is a group homomorphism.[/step]

[guided]We want to verify $f_*([\gamma_0] \cdot [\gamma_1]) = f_*([\gamma_0]) \cdot f_*([\gamma_1])$. The core observation is that $f$ **commutes with concatenation on the nose** — that is, $f \circ (\gamma_0 \cdot \gamma_1)$ and $(f \circ \gamma_0) \cdot (f \circ \gamma_1)$ are literally the same function $I \to Y$, not merely homotopic. Why on the nose? Concatenation is a **piecewise** definition: first half is $\gamma_0$ at double speed, second half is $\gamma_1$ at double speed. Postcomposing with $f$ acts pointwise, so each piece just gets an $f$ applied to its output: \begin{align*} f(\gamma_0 \cdot \gamma_1)(s) = f\bigl(\gamma_0 \cdot \gamma_1(s)\bigr) = \begin{cases} f(\gamma_0(2s)) & s \le 1/2 \\ f(\gamma_1(2s - 1)) & s \ge 1/2 \end{cases} \end{align*} which is $(f \circ \gamma_0) \cdot (f \circ \gamma_1)$ by the same concatenation formula applied to the postcomposed loops. With strict equality $f \circ (\gamma_0 \cdot \gamma_1) = (f \circ \gamma_0) \cdot (f \circ \gamma_1)$ in hand, the homomorphism property falls out by unwinding definitions: \begin{align*} f_*([\gamma_0] \cdot [\gamma_1]) = f_*([\gamma_0 \cdot \gamma_1]) = [f \circ (\gamma_0 \cdot \gamma_1)] = [(f \circ \gamma_0) \cdot (f \circ \gamma_1)] = [f \circ \gamma_0] \cdot [f \circ \gamma_1] = f_*([\gamma_0]) \cdot f_*([\gamma_1]). \end{align*} **The subtle point.** We used Step 2 of [Theorem 1878](/theorems/1878) (the well-definedness of the group law) implicitly in the second-to-last equality: $[\alpha] \cdot [\beta] = [\alpha \cdot \beta]$ requires that concatenation descend to classes. That was established in Theorem 1878.[/guided]

[step:Verify based-homotopy invariance $f \simeq f' \implies \pi_1(f) = \pi_1(f')$]Suppose $f \simeq f'$ as based maps, i.e., there exists a continuous map $H: X \times I \to Y$ with \begin{align*} H(x, 0) = f(x), \quad H(x, 1) = f'(x) \text{ for all } x \in X, \quad H(x_0, t) = y_0 \text{ for all } t \in I. \end{align*} Let $\gamma$ be a loop at $x_0$. Define \begin{align*} K: I \times I &\to Y \\ (s, t) &\mapsto H(\gamma(s), t). \end{align*} $K$ is the composition of the continuous map $(s, t) \mapsto (\gamma(s), t)$ with the continuous $H$, hence continuous. Its boundary values are \begin{align*} K(s, 0) = H(\gamma(s), 0) = f(\gamma(s)) = (f \circ \gamma)(s), \\ K(s, 1) = H(\gamma(s), 1) = f'(\gamma(s)) = (f' \circ \gamma)(s). \end{align*} At the endpoints of $I$ in the $s$-direction, using $\gamma(0) = \gamma(1) = x_0$ and the hypothesis $H(x_0, t) = y_0$, \begin{align*} K(0, t) = H(\gamma(0), t) = H(x_0, t) = y_0, \quad K(1, t) = H(\gamma(1), t) = H(x_0, t) = y_0 \text{ for all } t \in I. \end{align*} Thus $K$ is a path homotopy from $f \circ \gamma$ to $f' \circ \gamma$ rel $\{0, 1\}$, so $[f \circ \gamma] = [f' \circ \gamma]$ in $\pi_1(Y, y_0)$. That is, $\pi_1(f)([\gamma]) = \pi_1(f')([\gamma])$ for every class, and therefore $\pi_1(f) = \pi_1(f')$.[/step]

[guided]This proof parallels the one for $\pi_0$ in [Theorem 1875](/theorems/1875), but now the homotopy must be **based**: $H$ is required to keep $x_0$ pinned to $y_0$ throughout. Otherwise the induced equality of loops could fail to be rel endpoints. For $[\gamma] \in \pi_1(X, x_0)$, we use $H$ to construct a path homotopy $K: I \times I \to Y$ between $f \circ \gamma$ and $f' \circ \gamma$. The natural formula is obtained by "tracking $\gamma$ through the homotopy": \begin{align*} K(s, t) := H(\gamma(s), t). \end{align*} This is continuous as a composition $I \times I \to X \times I \to Y$, where the first map is $(s, t) \mapsto (\gamma(s), t)$ (continuous because $\gamma$ is) and the second is $H$. The boundary values at $t = 0, 1$ immediately give $K(s, 0) = f(\gamma(s))$ and $K(s, 1) = f'(\gamma(s))$. The rel-$\{0, 1\}$ condition in the $s$-direction uses **both** that $\gamma$ is a loop (so $\gamma(0) = \gamma(1) = x_0$) and that $H$ is a based homotopy (so $H(x_0, t) = y_0$ for all $t$). Together: $K(0, t) = H(x_0, t) = y_0$, constant in $t$; same for $K(1, t)$. **What fails without basedness?** If $H$ were merely a free homotopy, then $K(0, t) = H(x_0, t)$ would in general move through $Y$ as $t$ varies, so $K$ would not be a path homotopy rel endpoints. This is precisely the distinction between free and based homotopy classes: $\pi_1$ is a based invariant, and the functorial homotopy invariance requires based homotopies of maps.[/guided]

[step:Verify composition and identity laws] Let $h: (X, x_0) \to (Y, y_0)$ and $k: (Y, y_0) \to (Z, z_0)$ be composable based maps. For any loop $\gamma$ at $x_0$, $(k \circ h) \circ \gamma = k \circ (h \circ \gamma)$ by associativity of function composition. Taking classes, \begin{align*} \pi_1(k \circ h)([\gamma]) = [(k \circ h) \circ \gamma] = [k \circ (h \circ \gamma)] = \pi_1(k)([h \circ \gamma]) = \pi_1(k)(\pi_1(h)([\gamma])) = (\pi_1(k) \circ \pi_1(h))([\gamma]). \end{align*} This holds for every class, so $\pi_1(k \circ h) = \pi_1(k) \circ \pi_1(h)$ as functions. For the identity, $\operatorname{id}_X \circ \gamma = \gamma$ as maps $I \to X$, so $\pi_1(\operatorname{id}_X)([\gamma]) = [\gamma] = \operatorname{id}_{\pi_1(X, x_0)}([\gamma])$ for every class, hence $\pi_1(\operatorname{id}_X) = \operatorname{id}_{\pi_1(X, x_0)}$. Both $\operatorname{id}_X$ and $\pi_1(\operatorname{id}_X)$ also preserve the basepoint data trivially. [/step]

[step:Conclude] Steps 1 and 2 produce a well-defined homomorphism $f_*: \pi_1(X, x_0) \to \pi_1(Y, y_0)$. Step 3 establishes based-homotopy invariance. Step 4 establishes the composition and identity laws. These together are exactly the assertion that $\pi_1$ is a functor from the based homotopy category of pointed [topological spaces](/pages/Topological%20Space) to the category of groups, completing the proof. [/step]