基本群

$H(s,t):=\gamma\bigl((1-t)\varphi(s)+ts\bigr)$ とおく。$(1-t)\varphi(s)+ts$ は $\varphi(s)$ と $s$ を結ぶ線分上の点なので $I$ に属し、$H$ は連続写像の合成として連続である。$H(s,0)=\gamma(\varphi(s))$、$H(s,1)=\gamma(s)$、$H(0,t)=\gamma(0)$、$H(1,t)=\gamma(1)$ である。$\square$

1. $H\colon\gamma_0\simeq\gamma_1$、$G\colon\delta_0\simeq\delta_1$ を道のホモトピーとし、
   $$ K(s,t):=\begin{cases}H(2s,t)&(0\le s\le1/2)\\ G(2s-1,t)&(1/2\le s\le1)\end{cases} $$
   とおく。$s=1/2$ では $H(1,t)=\gamma_0(1)=\delta_0(0)=G(0,t)$ で両式が一致するので、貼り合わせの補題により $K$ は $I\times I$ 上で連続である。$K(s,0)=(\gamma_0\cdot\delta_0)(s)$、$K(s,1)=(\gamma_1\cdot\delta_1)(s)$、$K(0,t)=H(0,t)=\gamma_0(0)$、$K(1,t)=G(1,t)=\delta_0(1)$ である。
2. $H\colon\gamma_0\simeq\gamma_1$ に対し $(s,t)\mapsto H(1-s,t)$ が $\bar\gamma_0$ から $\bar\gamma_1$ への道のホモトピーである。
3. $f\circ H$ が $f\circ\gamma_0$ から $f\circ\gamma_1$ への道のホモトピーである。後半の二つの等式は、道の積と逆の道の定義式に $f$ を合成すれば直ちに分かる。$\square$

1. 定義式を書き下すと
   $$ ((\gamma\cdot\delta)\cdot\varepsilon)(s)=\begin{cases}\gamma(4s)&(0\le s\le1/4)\\ \delta(4s-1)&(1/4\le s\le1/2)\\ \varepsilon(2s-1)&(1/2\le s\le1)\end{cases},\qquad (\gamma\cdot(\delta\cdot\varepsilon))(u)=\begin{cases}\gamma(2u)&(0\le u\le1/2)\\ \delta(4u-2)&(1/2\le u\le3/4)\\ \varepsilon(4u-3)&(3/4\le u\le1)\end{cases} $$
   である。$\varphi\colon I\to I$ を $\varphi(s)=2s$（$0\le s\le1/4$）、$s+1/4$（$1/4\le s\le1/2$）、$(s+1)/2$（$1/2\le s\le1$）で定めると、分点 $s=1/4,1/2$ で値が $1/2,3/4$ に一致するので $\varphi$ は連続であり、$\varphi(0)=0$、$\varphi(1)=1$ である。各区間で代入すると $(\gamma\cdot(\delta\cdot\varepsilon))\circ\varphi=(\gamma\cdot\delta)\cdot\varepsilon$ が確かめられる（たとえば $1/4\le s\le1/2$ では $\varphi(s)=s+1/4\in[1/2,3/4]$ で $\delta(4(s+1/4)-2)=\delta(4s-1)$）。よって fundamental-group-lem-reparam により $(\gamma\cdot\delta)\cdot\varepsilon\simeq\gamma\cdot(\delta\cdot\varepsilon)$ である。
2. $x:=\gamma(0)$ とすると $c_x\cdot\gamma=\gamma\circ\varphi$、$\varphi(s):=\max\{0,2s-1\}$ であり、$\varphi$ は連続で $\varphi(0)=0$、$\varphi(1)=1$ なので fundamental-group-lem-reparam により $c_x\cdot\gamma\simeq\gamma$ である。同様に $\gamma\cdot c_{\gamma(1)}=\gamma\circ\psi$、$\psi(s):=\min\{2s,1\}$ から $\gamma\cdot c_{\gamma(1)}\simeq\gamma$ を得る。
3. $\lambda(s):=\min\{2s,2-2s\}$ とおくと $\gamma\cdot\bar\gamma=\gamma\circ\lambda$ である（$s\ge1/2$ では $\bar\gamma(2s-1)=\gamma(2-2s)$）。$H(s,t):=\gamma\bigl((1-t)\lambda(s)\bigr)$ は連続で、$H(s,0)=(\gamma\cdot\bar\gamma)(s)$、$H(s,1)=\gamma(0)$、$H(0,t)=H(1,t)=\gamma(0)$ である（$\lambda(0)=\lambda(1)=0$）。よって $\gamma\cdot\bar\gamma\simeq c_{\gamma(0)}$ である。これを $\bar\gamma$ に適用し $\bar{\bar\gamma}=\gamma$ に注意すれば $\bar\gamma\cdot\gamma\simeq c_{\gamma(1)}$ を得る。
   最後の主張：積が類の上で定まることは fundamental-group-prop-welldefined (1) による。(1)〜(3) をループに適用すれば群の公理そのものである。$\square$

1. $f\circ\gamma$ が $y_0$ を基点とするループであることと、$f_*$ が代表元によらないことは fundamental-group-prop-welldefined (3) による。同じ (3) の等式 $f\circ(\gamma\cdot\delta)=(f\circ\gamma)\cdot(f\circ\delta)$ から $f_*([\gamma][\delta])=f_*[\gamma]\,f_*[\delta]$ である。
2. $(g\circ f)_*[\gamma]=[g\circ f\circ\gamma]=g_*[f\circ\gamma]=g_*(f_*[\gamma])$、$(\operatorname{id}_X)_*[\gamma]=[\gamma]$ である。$\square$

以下、道の積の等式・ホモトピーはすべて fundamental-group-thm-group と fundamental-group-prop-welldefined による。
(1) $\gamma\simeq\gamma'$ なら $\bar C\cdot\gamma\cdot C\simeq\bar C\cdot\gamma'\cdot C$ なので $\Phi_C$ は矛盾なく定まる。準同型性は
$$ \Phi_C[\gamma]\,\Phi_C[\delta]=[\bar C\cdot\gamma\cdot C\cdot\bar C\cdot\delta\cdot C]=[\bar C\cdot\gamma\cdot c_x\cdot\delta\cdot C]=[\bar C\cdot(\gamma\cdot\delta)\cdot C]=\Phi_C[\gamma\cdot\delta] $$
による。$\Phi_{\bar C}\colon\pi_1(X,y)\to\pi_1(X,x)$ を同様に定めると（$\bar{\bar C}=C$）、$\Phi_{\bar C}\Phi_C[\gamma]=[C\cdot\bar C\cdot\gamma\cdot C\cdot\bar C]=[c_x\cdot\gamma\cdot c_x]=[\gamma]$ であり、同様に $\Phi_C\Phi_{\bar C}=\operatorname{id}$ である。$X$ が弧状連結なら任意の二点は道で結べるので、後半が従う。
(2) $C\simeq C'$ なら $\bar C\simeq\bar C'$ でもあり、$\bar C\cdot\gamma\cdot C\simeq\bar C'\cdot\gamma\cdot C'$ である。$\overline{C\cdot D}=\bar D\cdot\bar C$ が等号で成り立つ（定義式を代入すればよい）ので、$\Phi_{C\cdot D}[\gamma]=[\bar D\cdot\bar C\cdot\gamma\cdot C\cdot D]=\Phi_D(\Phi_C[\gamma])$ である。
(3) $C$ がループなら $[\bar C]=[C]^{-1}$ なので前半は定義そのものである。$C,C'$ を $x$ から $y$ への道とすると、$C'\simeq(C'\cdot\bar C)\cdot C$ であり $C'\cdot\bar C$ は $x$ のループなので、(2) により $\Phi_{C'}=\Phi_C\circ\Phi_{C'\cdot\bar C}$ である。$\pi_1(X,x)$ がアーベル群なら内部自己同型 $\Phi_{C'\cdot\bar C}$ は恒等写像であり、$\Phi_{C'}=\Phi_C$ を得る。$\square$

1. $\gamma$ を $x_0$ のループとする。$u\in I$ に対し $C_u(t):=C(ut)$（$f(x_0)$ から $C(u)$ への道）、$F_u:=F(\cdot,u)$ とおくと、$F_u\circ\gamma$ は $F(x_0,u)=C(u)$ のループであり、
   $$ L_u:=C_u\cdot\bigl((F_u\circ\gamma)\cdot\overline{C_u}\bigr) $$
   は $f(x_0)$ のループである。$K(s,u):=L_u(s)$ とおくと、$K$ は $s\le1/2$ で $C(2us)$、$1/2\le s\le3/4$ で $F(\gamma(4s-2),u)$、$s\ge3/4$ で $C(u(4-4s))$ という三つの連続な式の貼り合わせであり、境目 $s=1/2$、$s=3/4$ で値はいずれも $C(u)$ に一致するので、貼り合わせの補題により $I\times I$ 上で連続である。さらに $K(0,u)=K(1,u)=C(0)=f(x_0)$ なので、$K$ は $L_0$ から $L_1$ への道のホモトピーである。$L_0=c\cdot((f\circ\gamma)\cdot c)\simeq f\circ\gamma$（$c$ は定値道、fundamental-group-thm-group (2)）であり、$L_1=C\cdot((g\circ\gamma)\cdot\bar C)$ である。よって $[f\circ\gamma]=[C][g\circ\gamma][C]^{-1}$、すなわち $g_*[\gamma]=[\bar C\cdot(f\circ\gamma)\cdot C]=\Phi_C(f_*[\gamma])$ である。
2. 基点を固定したホモトピーでは $C$ は定値道であり、$\Phi_C=\operatorname{id}$ である。$g\colon Y\to X$ を $f$ のホモトピー逆写像とし、$F\colon\operatorname{id}_X\simeq g\circ f$、$G\colon\operatorname{id}_Y\simeq f\circ g$ をとる。(1) を $F$ と $x_0$ に適用すると $(g\circ f)_*=\Phi_C\circ(\operatorname{id}_X)_*=\Phi_C$（$C$ は $x_0$ から $gf(x_0)$ への軌跡）が同型なので、fundamental-group-prop-functorial により $g_*\circ f_*$ は同型であり、$f_*\colon\pi_1(X,x_0)\to\pi_1(Y,f(x_0))$ は単射、$g_*\colon\pi_1(Y,f(x_0))\to\pi_1(X,gf(x_0))$ は全射である。同様に (1) を $G$ と基点 $f(x_0)$ に適用すると $f_*\circ g_*\colon\pi_1(Y,f(x_0))\to\pi_1(Y,fgf(x_0))$ が同型なので、この $g_*$ は単射でもある。よって $g_*$ は同型であり、$f_*=(g_*)^{-1}\circ(g_*\circ f_*)$ も同型である。
3. $u\in I$ に対し $D_u(t):=C(ut)$（$x_0$ から $C(u)$ への道）とおき、$C(u)$ のループ $N_u:=\overline{D_u}\cdot(\gamma\cdot D_u)$ を考える。$K(s,u):=N_u(s)$ は (1) と同様に三つの連続な式の貼り合わせで連続であり、$K(0,u)=K(1,u)=C(u)$ である。$N_0=c_{x_0}\cdot(\gamma\cdot c_{x_0})$ は $\gamma$ と道としてホモトピックであり、$N_1=\bar C\cdot(\gamma\cdot C)$ は $\bar C\cdot\gamma\cdot C$ と道としてホモトピックである（fundamental-group-thm-group (1)(2)）。道のホモトピーは端点を止めるホモトピーであるから、この二つの道のホモトピーと上の $K$ を $t$ 方向に（ホモトピーの記事の命題「ホモトピー関係は同値関係」の推移律の証明と）同じ貼り合わせによりつなげば、各時刻で $K(0,t)=K(1,t)$ が保たれ、求める $K$ が得られる。$\square$

$p_*,q_*$ は準同型なので $(p_*,q_*)$ は直積群への準同型である。全射性：$\alpha$ を $x_0$ のループ、$\beta$ を $y_0$ のループとすると、直積位相の普遍性により $\gamma:=(\alpha,\beta)\colon I\to X\times Y$ は連続で、$(x_0,y_0)$ のループであり、$p\circ\gamma=\alpha$、$q\circ\gamma=\beta$ である。単射性：$[p\circ\gamma]=[c_{x_0}]$、$[q\circ\gamma]=[c_{y_0}]$ とし、道のホモトピー $H_1\colon p\circ\gamma\simeq c_{x_0}$、$H_2\colon q\circ\gamma\simeq c_{y_0}$ をとる。$H(s,t):=(H_1(s,t),H_2(s,t))$ は連続で、$H(s,0)=\gamma(s)$、$H(s,1)=(x_0,y_0)$、$H(0,t)=H(1,t)=(x_0,y_0)$ を満たすので $[\gamma]=[c_{(x_0,y_0)}]$ である。$\square$

$p$ が被覆写像であることは被覆空間の記事の例「円周を実数直線で覆う」による。以下、同記事の定理「道の持ち上げ」（始点を指定した持ち上げの存在と一意性）と系「道のホモトピー類と持ち上げの終点」（道としてホモトピックな二つの道の、同じ始点からの持ち上げは同じ終点をもつ）を用いる。$\deg$ が矛盾なく定まること（well-defined 性）はこの系に依り、同系はホモトピーの持ち上げ（同記事が Hat02 Proposition 1.30 を引用する）に依る。
矛盾なく定まること：持ち上げ $\tilde\gamma$ は一意に存在し、$p(\tilde\gamma(1))=\gamma(1)=b_0$ から $\tilde\gamma(1)\in p^{-1}(b_0)=\mathbb{Z}$ である。$\gamma\simeq\gamma'$ なら上の系により $\tilde\gamma(1)=\tilde\gamma'(1)$ である。
準同型性：$\gamma,\delta$ を $b_0$ のループ、$m:=\deg\gamma$、$n:=\deg\delta$ とする。$\tau(s):=\tilde\gamma(2s)$（$s\le1/2$）、$\tilde\delta(2s-1)+m$（$s\ge1/2$）とおくと、$s=1/2$ で $\tilde\gamma(1)=m=\tilde\delta(0)+m$ と一致するので $\tau$ は $0$ を始点とする $\mathbb{R}$ の道であり、$p(t+m)=p(t)$ から $p\circ\tau=\gamma\cdot\delta$ である。一意性により $\tau$ が $\gamma\cdot\delta$ の持ち上げなので、$\deg(\gamma\cdot\delta)=\tau(1)=n+m$ である。
全射性：$n\in\mathbb{Z}$ に対し $\omega_n(s):=(\cos2\pi ns,\sin2\pi ns)$ は $s\mapsto ns$ を持ち上げにもつので $\deg\omega_n=n$ である。とくに $\deg\omega=1$ であり、$[\omega]$ が生成元である。
単射性：$\deg\gamma=0$ とすると $\tilde\gamma$ は $0$ を基点とする $\mathbb{R}$ のループである。$H(s,t):=(1-t)\tilde\gamma(s)$ は連続で、$H(s,0)=\tilde\gamma(s)$、$H(s,1)=0$、$H(0,t)=H(1,t)=0$ を満たすので、$p\circ H$ は $\gamma=p\circ\tilde\gamma$ から定値ループ $c_{b_0}$ への道のホモトピーである。よって $[\gamma]$ は単位元である。$\square$