The fibration connecting map is independent of lift and representative

A relative representative $a$ has $pa=b_0$ on its entire boundary because $a(t=0)\subseteq F$ and $a{\mathrm{\mid }}_J=e_0$. Relative homotopies similarly project to based homotopies. Thus composition defines the displayed pointed map; for $n\ge 2$ it preserves coordinate-one concatenation by F2. Given an absolute representative $b$ in $B$, F1 constructs a lift constant on $J$, hence a relative representative with projection exactly $b$. This proves surjectivity in every degree, including $n=1$.

Suppose relative representatives $a_0,a_1$ have based-homotopic projections, through $b(u,t,r)$, $r\in I$. Treat $(u,r)\in I^{n-1}\times I$ as the parameter disk and lift in reversed $t$-time. At $t=1$ prescribe $e_0$ everywhere. On the parameter boundary prescribe $a_0(u,t)$ at $r=0$, $a_1(u,t)$ at $r=1$, and $e_0$ on $u\in \mathrm{\partial }{I}^{n-1}$. These prescriptions agree on intersections, and project to $b$ there because the base homotopy is based. F3 extends them over the full cylinder. At $t=0$ the lift lies in $F$, since $b(u,0,r)=b_0$; on every $J$ face it is $e_0$. It is therefore a relative homotopy from $a_0$ to $a_1$. For $n=1$ the parameter disk is just the $r$ interval and its two endpoints carry the two given paths, so the same argument proves injectivity of pointed sets.

Steps 1.1–1.2 prove bijectivity. The connecting map equals the relative boundary map of F2 composed with the inverse bijection. Consequently both arbitrary lift choices and representative changes give the same output. For $n\ge 2$ a bijective homomorphism has a homomorphic inverse, so this composite is a homomorphism. For $n=1$ it is a pointed map: the constant base representative admits the constant $e_0$ lift, whose initial component is distinguished.

Specifying $e_0$ excludes empty fibers and empty total/base spaces; zero-dimensional boundary cubes when $n=1$ record points, not a nonexistent relative ${\pi }_0$. Constant cubes and point spaces are included by the same construction. All extension domains above are finite cubes with finite subcomplexes; F3 therefore uses only finitely many existential witnesses, and no AC. The equations at $t=0,1$ and $r=0,1$ establish every required endpoint condition.