[proofplan] We prove the composition law by translating maximal solutions in time. First, the solution through $x_0$ shifted by $s$ is a solution through $\varphi(s,x_0)$ on the shifted interval $J_{x_0}-s$, so maximality gives one inclusion of domains. For the reverse inclusion, we compare the maximal solution through $\varphi(s,x_0)$ with the original solution near the time $s$, then patch the two solutions to produce an extension of the maximal solution through $x_0$. Maximality forces the patched domain to lie inside $J_{x_0}$, giving the reverse inclusion and hence the flow identity. [/proofplan] [step:Shift the maximal solution through $x_0$ to obtain a solution through $\varphi(s,x_0)$] Define \begin{align*} \gamma:J_{x_0}\to U \end{align*} by $\gamma(r)=\varphi(r,x_0)$. By definition of the maximal flow, $\gamma$ is the maximal solution of $\dot{x}=f(x)$ with $\gamma(0)=x_0$. Define the shifted interval \begin{align*} L:=J_{x_0}-s=\{t\in\mathbb{R}:t+s\in J_{x_0}\}. \end{align*} Since $s\in J_{x_0}$, we have $0\in L$. Define \begin{align*} \eta:L\to U \end{align*} by $\eta(t)=\gamma(t+s)$. The map $\eta$ is continuous because $\gamma$ is continuous. At every interior point $t\in L$, the point $t+s$ is an interior point of $J_{x_0}$, and the chain rule for the translation map $t\mapsto t+s$ gives \begin{align*} \dot{\eta}(t)=\dot{\gamma}(t+s)=f(\gamma(t+s))=f(\eta(t)). \end{align*} At endpoints of $L$, the same computation holds with the corresponding one-sided derivative because translation preserves one-sided limits. Also \begin{align*} \eta(0)=\gamma(s)=\varphi(s,x_0). \end{align*} Thus $\eta$ is a solution through $\varphi(s,x_0)$ on $L$. [/step] [step:Use maximality through $\varphi(s,x_0)$ to get the first domain inclusion] Let \begin{align*} y:=\varphi(s,x_0). \end{align*} The map $\eta:L\to U$ constructed above is a solution of $\dot{x}=f(x)$ with initial value $\eta(0)=y$. Define $F:\mathbb{R}\times U\to \mathbb{R}^n$ by $F(t,x)=f(x)$. Since $U$ is open, $F$ is continuous and locally Lipschitz in the state variable, so the hypotheses of [citetheorem:8313] apply with ambient time interval $\mathbb{R}$, state space $U$, and initial datum $(0,y)$. The theorem gives a unique maximal solution through $y$ and states that every other solution through $y$ is the restriction of that maximal solution to its interval of definition. Applying this extension conclusion to $\eta$ gives \begin{align*} L\subset J_y \end{align*} and \begin{align*} \varphi(t,y)=\eta(t)=\gamma(t+s)=\varphi(t+s,x_0) \end{align*} for every $t\in L$. [guided] The shifted curve $\eta$ is not merely a convenient notation: it is an honest solution with initial value $y=\varphi(s,x_0)$. To invoke the maximal existence theorem precisely, define $F:\mathbb{R}\times U\to \mathbb{R}^n$ by $F(t,x)=f(x)$. The set $U$ is open by hypothesis, and because $f$ is locally Lipschitz, the map $F$ is continuous and locally Lipschitz in the state variable. Therefore [citetheorem:8313] applies with ambient time interval $\mathbb{R}$, state space $U$, and initial datum $(0,y)$. Its extension property says that every solution with initial value $y$ is contained in the unique maximal solution through $y$. We apply that result to the solution \begin{align*} \eta:L\to U. \end{align*} Because $\eta(0)=y$, maximality of the flow line $t\mapsto \varphi(t,y)$ gives \begin{align*} L\subset J_y. \end{align*} On this common domain, uniqueness also gives equality of the two solutions: \begin{align*} \varphi(t,y)=\eta(t). \end{align*} Substituting the definition of $\eta$ and then the definition of $\gamma$ gives \begin{align*} \varphi(t,y)=\eta(t)=\gamma(t+s)=\varphi(t+s,x_0). \end{align*} Thus every time $t$ for which $t+s\in J_{x_0}$ is also a valid time for the flow starting at $y$, and the desired composition identity already holds on $J_{x_0}-s$. [/guided] [/step] [step:Patch the two solution curves to force the reverse domain inclusion] Let \begin{align*} z:J_y\to U \end{align*} be the maximal solution through $y$, so $z(t)=\varphi(t,y)$ and $z(0)=y$. Define the translated interval \begin{align*} M:=s+J_y=\{r\in\mathbb{R}:r-s\in J_y\}. \end{align*} Since $0\in J_y$, we have $s\in M$. Define \begin{align*} \zeta:M\to U \end{align*} by $\zeta(r)=z(r-s)$. By the same translation argument as before, $\zeta$ is a solution of $\dot{x}=f(x)$ on $M$, and \begin{align*} \zeta(s)=z(0)=y=\gamma(s). \end{align*} The intervals $J_{x_0}$ and $M$ both contain $s$. Since both are intervals in $\mathbb{R}$, their union $J_{x_0}\cup M$ is again an interval. On the intersection $J_{x_0}\cap M$, the two solutions $\gamma$ and $\zeta$ solve the same autonomous equation and agree at $s$. The hypotheses of [citetheorem:8313] apply as above to $F(t,x)=f(x)$, and its uniqueness conclusion gives \begin{align*} \gamma(r)=\zeta(r) \end{align*} for every $r\in J_{x_0}\cap M$. Define \begin{align*} \beta:J_{x_0}\cup M\to U \end{align*} by setting $\beta(r)=\gamma(r)$ for $r\in J_{x_0}$ and $\beta(r)=\zeta(r)$ for $r\in M$. The preceding equality on $J_{x_0}\cap M$ shows that $\beta$ is well-defined. On each of the open pieces where it is represented by $\gamma$ or by $\zeta$, it satisfies $\dot{\beta}=f(\beta)$. At points of $J_{x_0}\cap M$, the two representatives agree on a neighbourhood inside the overlap, so their derivatives agree there as well; at endpoints belonging to the union the same statement holds with the corresponding one-sided derivative. Hence $\beta$ is a solution of $\dot{x}=f(x)$ on the interval $J_{x_0}\cup M$, with $\beta(0)=\gamma(0)=x_0$. By the extension conclusion of [citetheorem:8313], the domain of any solution through $x_0$ is contained in the maximal interval $J_{x_0}$. Therefore \begin{align*} J_{x_0}\cup M\subset J_{x_0}. \end{align*} Hence $M\subset J_{x_0}$. [/step] [step:Translate the two inclusions into equality of maximal intervals and the composition law] The inclusion obtained in the second step says \begin{align*} J_{x_0}-s\subset J_y. \end{align*} The inclusion $M\subset J_{x_0}$ obtained in the previous step says that if $r=s+t$ with $t\in J_y$, then $r\in J_{x_0}$. Equivalently, \begin{align*} J_y\subset J_{x_0}-s. \end{align*} Thus \begin{align*} J_y=J_{x_0}-s. \end{align*} Since $y=\varphi(s,x_0)$, this is exactly \begin{align*} J_{\varphi(s,x_0)}=J_{x_0}-s. \end{align*} Finally, for any $t\in J_{\varphi(s,x_0)}$, the equality of intervals gives $t+s\in J_{x_0}$. The identity already proved on $J_{x_0}-s$ gives \begin{align*} \varphi(t,\varphi(s,x_0))=\varphi(t+s,x_0). \end{align*} This proves the stated flow composition law. [/step]