An integral curve of an i-related field that starts at the image of the starting point of an interior integral curve is the image of that curve

Let $M$ and $N$ be Hausdorff smooth 3-manifolds with boundary (modelled on the closed half-space), let $X$ be a C¹ vector field on $M$ and $Z$ a vector field on $N$, and let $i:M\to N$ be a C¹ map that is a topological embedding, has an injective derivative at every point, and carries $X$ to $Z$:

An integral curve of $X$ on a set of times $S\subseteq\mathbb R$ is a curve $\gamma:\mathbb R\to M$ whose derivative within $S$ at every $u\in S$ is $X(\gamma(u))$ (Mathlib's IsMIntegralCurveOn; at the endpoints of an interval the derivative is one-sided). We write $[0,t]$ for the closed interval between $0$ and $t$, in either order (Mathlib's uIcc 0 t). Let $\delta$ be an integral curve of $X$ on $[0,t]$ all of whose points $\delta(s)$, $s\in[0,t]$, are interior points of $M$, and let $\gamma$ be an integral curve of $Z$ on $[0,t]$ with $\gamma(0)=i(\delta(0))$. Then

In words: an integral curve of $Z$ that starts at $i(\delta(0))$, where $\delta$ is an integral curve of $X$ through interior points of $M$, equals $i\circ\delta$ on the whole time interval; in particular it does not leave $i(M)$. The intended proof lifts $\gamma$ through $i$ on short time spans (the companion lemma integralCurve_lift_of_embedding, proved earlier in this mission), uses that $i(M)$ is a neighbourhood of each $i(\delta(s))$ (range_mem_nhds_of_isInteriorPoint) and the uniqueness statement isMIntegralCurveOn_uIcc_eq, and extends the agreement over the whole interval by a closed-and-open argument. A general fact, not stated in the paper; it is one of the facts behind footnote 2 of Section 1 (p. 2 of arXiv v1: the differentiable structure on W is compatible with those of U and V by restriction) and behind the fourth and fifth sentences of the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14), which state without proof that Λ_Z contains Λ_X and Λ_Y (through the inclusions) and use, without comment, that Λ_X and Λ_Y are hyperbolic sets of Z. In the proof of plugGluing_local_conjugacy it identifies the integral curve of $Z$ chosen by the time-$t$ map at $i_U(y)$ with the image of the orbit of $y$ under $X$.

Formalization Note $Z$ is not assumed to be C¹ or even continuous; its curves are controlled only through the embedding. The Hausdorff hypotheses are used for the closedness of the set of agreement times and in the uniqueness statement. No compactness is assumed.