Long exact sequence of homotopy groups of a fibration

Replace each relative term ${\pi }_n(E,F)$ of F2 by ${\pi }_n(B)$ using F1. The composite from ${\pi }_n(E)$ is actual composition with $p$, since the relative representative is the same cube. The outgoing map is exactly ${\mathrm{\partial }}_p$ by F1. Bijections preserve inverse images of distinguished points and images; in group degrees F1 gives group isomorphisms. F2 therefore proves the displayed exactness through ${\pi }_0(F)$, including ${\pi }_1(B)$ with a pointed-set outgoing map.

A component of $E$ containing a fiber point maps to $[b_0]$. Conversely, if $p(e)$ is joined to $b_0$, lift a path from $p(e)$ to $b_0$ starting at $e$ using F4. Its endpoint is in $F$ and in the component of $e$. This proves exactness at ${\pi }_0(E)$. The image of the last arrow is by definition the set of components meeting $p(E)$, proving the precise surjectivity criterion.

To verify the proposed action, first fix a path $\gamma$ and two lifts whose initial points are joined by a path in its initial fiber. More generally let the base paths vary through an endpoint-fixed homotopy. On a square prescribe the two given lifts on its vertical sides and the given initial fiber path on its bottom. F4 extends the lift, using base path time as lifting time and the other coordinate as parameter. The top is a path in the terminal fiber, so the endpoint components agree. This proves simultaneous independence of the initial point within its component, of the lift, and of the endpoint-fixed base representative. Existence is path lifting.

The constant lift proves the identity law on components. Pasting a lift of $\gamma$ with a lift of $\eta$ starting at its endpoint gives a lift of $\gamma \ast \eta$. Step 1.3 therefore proves $([e]\cdot [\gamma ])\cdot [\eta ]=[e]\cdot ([\gamma ][\eta ])$. Reversal gives inverses. If a loop in $E$ is based at $e_0$, it exhibits that its projected loop stabilizes $[e_0]$. Conversely, for a stabilizing base loop, lift it from $e_0$ and join its endpoint to $e_0$ in $F$. Pasting gives a based loop of $E$ whose projection is the original loop with a constant segment, hence the same based class. Thus the stabilizer is exactly the claimed image.

Points related by the action are connected in $E$ by a lifted loop, with possible fiber paths. Conversely a path in $E$ between two points of $F$ projects to a loop at $b_0$ and witnesses the corresponding action relation. Thus orbits are exactly fibers of $i_{\ast }$, even when $E$ or $F$ is disconnected. A lift of $\gamma$ ending at $e_0$, read backwards, is a lift of ${\gamma }^{-1}$ starting there. Its initial component is therefore $[e_0]\cdot [\gamma {]}^{-1}$ by step 1.3, proving the boundary formula.

The specified $e_0$ makes $E,B,F$ nonempty, but other base components may have empty fibers; step 1.2 explicitly allows this. In degree one the boundary is a component and no group structure on ${\pi }_0(F)$ is asserted. For a one-point or path-connected fiber its component action is trivial. All extra lifting problems use a point or finite square, and uniqueness of the resulting component defines the action without choosing a family of lifts. The preceding steps prove exactness, action laws, and all low-degree qualifications.