A smooth Cauchy hypersurface gives a connected timelike-flow product

If $E$ is empty, so is $C$, and the empty flow and product map give every conclusion, with the normal-derivative condition vacuous. Otherwise [F2] gives connectedness of $C$. Apply the density, volume-time and temporal-splitting suppliers in [F5] to $E$, with the conventions and choice assumptions of [F1], obtaining $Z$, $\mathrm{\Phi }$, $\tau$ and $\mathrm{\Psi }$ as stated there.

For any $p\in E$, write $p=\mathrm{\Psi }(a,z)={\mathrm{\Phi }}_a(z)$ using [F5]. Then [F4] and [F5] give $\tau ({\mathrm{\Phi }}_s(p))=\tau ({\mathrm{\Phi }}_{s+a}(z))=s+a=\tau (p)+s$. Hence neither parameter end of the future timelike orbit $s\mapsto {\mathrm{\Phi }}_s(p)$ converges to a point of $E$: continuity of $\tau$ would contradict this divergence. By [F1] the orbit is inextendible and meets $C$ at exactly one parameter value. Define $F(s,c)={\mathrm{\Phi }}_s(c)$. Every point lies on such an orbit, so $F$ is surjective. If $F(s,c)=F(r,d)$, the flow law gives $d={\mathrm{\Phi }}_{s-r}(c)$. Since the orbit of $c$ meets $C$ at the unique parameter value zero, $s=r$ and $d=c$. Thus $F$ is bijective and $F(0,c)=c$.

The map $F$ is smooth in the product structure of [F3], since it is the restriction of the smooth flow to the embedded section. By the flow law and chain rule in [F4], its differential is $d{F}_{(s,c)}(a,v)=(d{\mathrm{\Phi }}_s{)}_c(a{Z}_c+v)$ for $a\in \mathbb{R}$ and $v\in T_{c}C$. The map $d{\mathrm{\Phi }}_s$ is invertible, since ${\mathrm{\Phi }}_{-s}$ is its smooth inverse. A timelike vector cannot lie in the positive-definite three-plane $T_{c}C$, so $(a,v)\mapsto a{Z}_c+v$ is a linear isomorphism onto $T_{c}E$. Thus $dF$ is invertible everywhere. By [F6] local smooth inverses exist, and bijectivity makes them agree with the global inverse. Therefore $F$ is a diffeomorphism.

Put $\rho ={\mathrm{pr}}_1\circ F^{-1}$, smooth by [F3] and step 3.1. Since $F(0,c)=c$ and $F$ is bijective, ${\rho }^{-1}(0)=C$, and $\rho ({\mathrm{\Phi }}_s(c))=s$ for every $c\in C$.

On $C$, the function $\rho$ is identically zero. Restricting to the section and applying the differential and chain rule in [F4] shows that $d\rho$ annihilates $TC$. Differentiating $\rho ({\mathrm{\Phi }}_s(c))=s$ at zero with the integral-curve law gives $d\rho (Z)=1$. Decompose $Z=\alpha n+V$ there by [F1], with $V\in TC$ and $\alpha =-g(Z,n)$. In a Lorentz-orthonormal frame with future unit time vector $n$, the future timelike vector $Z$ has positive time component, so $\alpha >0$. Consequently $1=d\rho (Z)=\alpha d\rho (n)$ and $d\rho (n)=1\mathrm{/}\alpha >0$. This calculation uses the auxiliary timelike field and makes no identification with a stationary field.