Seifert–van Kampen identifies the fundamental group with a group pushout

Choose the pushout $P$ supplied by [L3]. The two inclusion-induced homomorphisms from ${\pi }_1(U,x_0)$ and ${\pi }_1(V,x_0)$ to ${\pi }_1(X,x_0)$ agree on ${\pi }_1(U\cap V,x_0)$, since both composites are induced by the same inclusion. By [F1], they therefore define a unique homomorphism $\mathrm{\Phi }:P\to {\pi }_1(X,x_0)$ satisfying $\mathrm{\Phi }{i}_U=(j_U{)}_{\ast }$ and $\mathrm{\Phi }{i}_V=(j_V{)}_{\ast }$.

For $c\in {\pi }_1(X,x_0)$, let $\mathrm{\Psi }(c)$ be the element of $P$ that is the value of some subordinate factorization of some loop representing $c$. Such a factorization exists by [L1], and [L2] says that all representatives and all their factorizations give the same value. Thus exactly one such element exists for each $c$, so this rule defines a function without selecting factorizations globally. Concatenating two factorizations concatenates their words, hence $\mathrm{\Psi }$ is a homomorphism.

If $c$ is represented by a factorized loop, applying $\mathrm{\Phi }$ to its pushout word restores the same product of inclusion-images, which is $c$ by [L1]. Hence $\mathrm{\Phi }\mathrm{\Psi }={\mathrm{id}}_{{\pi }_1(X,x_0)}$.

For $a\in {\pi }_1(U,x_0)$, the one-factor factorization of its image gives $\mathrm{\Psi }((j_U{)}_{\ast }a)=i_U(a)$, and similarly on the $V$ factor. Thus $\mathrm{\Psi }\mathrm{\Phi }:P\to P$ agrees with the identity after composition with both factor maps. Uniqueness in [F1] makes $\mathrm{\Psi }\mathrm{\Phi }={\mathrm{id}}_P$.

The homomorphisms $\mathrm{\Phi }$ and $\mathrm{\Psi }$ are inverse, so $\mathrm{\Phi }$ is an isomorphism and ${\pi }_1(X,x_0)$ has the asserted pushout property.