Kerodon

Proof. For $j \neq i$, choose an element $\sigma _{j} \in \Sigma $ satisfying $[ \sigma _ j ] = \eta _ j$. Then the tuple of $n$-simplices $( \sigma _0, \ldots , \sigma _{i-1}, \bullet , \sigma _{i+1}, \ldots , \sigma _{n+1} )$ determines a map of simplicial sets $f_0: \Lambda ^{n+1}_{i} \rightarrow X$ (see Proposition 1.2.4.7). Since $X$ is a Kan complex, we can extend $f_{0}$ to an $(n+1)$-simplex $\tau $ of $X$. Then $\eta _{i} = [ d^{n+1}_ i( \tau ) ]$ has the property that the tuple $\vec{\eta } = ( \eta _0, \eta _1, \ldots , \eta _{n+1} )$ bounds. This proves existence. To prove uniqueness, suppose we are given another element $\eta '_{i} \in \pi _{n}(X,x)$ for which the tuple $( \eta _0, \ldots , \eta _{i-1}, \eta '_{i}, \eta _{i+1}, \ldots , \eta _{n+1} )$ bounds. Write $\eta '_{i} = [ \sigma '_{i} ]$ for some $\sigma '_{i} \in \Sigma $, so that we can choose a simplex $\tau ': \Delta ^{n+1} \rightarrow X$ satisfying

Since the inclusion $\Lambda ^{n+1}_{i} \hookrightarrow \Delta ^{n+1}$ is anodyne, so the restriction map $\operatorname{Fun}( \Delta ^{n+1}, X) \rightarrow \operatorname{Fun}( \Lambda ^{n+1}_{i}, X)$ is a trivial Kan fibration (Corollary 3.1.3.6). It follows that there exists a homotopy from $\tau $ to $\tau '$ which is constant along the subset $\Lambda ^{n+1}_{i} \subseteq \Delta ^{n+1}$, so that $\eta _ i = [ d^{n+1}_ i( \tau ) ] = [ d^{n+1}_ i( \tau ' ) ] = \eta '_ i$. $\square$