The Stacks project

Proof. Let $\xi = (\gamma _ X) \in \prod \text{Aut}(F(X))$ be an element not in $\text{Aut}(F)$. Then there exists a morphism $f : X \to X'$ of $\mathcal{C}$ and an element $x \in F(X)$ such that $F(f)(\gamma _ X(x)) \not= \gamma _{X'}(F(f)(x))$. Consider the open neighbourhood $U = \{ \gamma \in \text{Aut}(F(X)) \mid \gamma (x) = \gamma _ X(x)\} $ of $\gamma _ X$ and the open neighbourhood $U' = \{ \gamma ' \in \text{Aut}(F(X')) \mid \gamma '(F(f)(x)) = \gamma _{X'}(F(f)(x))\} $. Then $U \times U' \times \prod _{X'' \not= X, X'} \text{Aut}(F(X''))$ is an open neighbourhood of $\xi $ not meeting $\text{Aut}(F)$. The final statement follows from the fact that $\prod \text{Aut}(F(X))$ is a profinite space if each $F(X)$ is finite. $\square$