1162: Subset of C∞ Manifold with Boundary That Satisfies Local-Slice-or-Half-Slice Condition Is Embedded Submanifold with Boundary with Subspace Topology and Adopting Atlas

<The previous article in this series | The table of contents of this series | The next article in this series>

description/proof of that subset of $C^{\mathrm{\infty }}$ manifold with boundary that satisfies local-slice-or-half-slice condition is embedded submanifold with boundary with subspace topology and adopting atlas

---

Topics

About: $C^{\mathrm{\infty }}$ manifold

---

The table of contents of this article

• Starting Context
• Target Context
• Orientation
• Main Body
• 1: Structured Description
• 2: Proof

---

Starting Context

• The reader knows a definition of subset of $C^{\mathrm{\infty }}$ manifold with boundary that satisfies local-slice-or-half-slice condition.
• The reader knows a definition of embedded submanifold with boundary of $C^{\mathrm{\infty }}$ manifold with boundary.
• The reader knows a definition of locally topologically closed upper half Euclidean topological space.
• The reader admits the proposition that any subspace of any Hausdorff topological space is Hausdorff.
• The reader admits the proposition that any subspace of any 2nd countable topological space is 2nd countable.
• The reader admits the proposition that for any maps between any arbitrary subsets of any $C^{\mathrm{\infty }}$ manifolds with boundary $C^k$ at corresponding points, where $k$ includes $\mathrm{\infty }$, the composition is $C^k$ at the point.
• The reader admits the proposition that for any $C^{\mathrm{\infty }}$ map between any $C^{\mathrm{\infty }}$ manifolds with boundary and any corresponding charts, the components function of the differential of the map with respect to the standard bases is this.

---

Target Context

• The reader will have a description and a proof of the proposition that any subset of any $C^{\mathrm{\infty }}$ manifold with boundary that satisfies the local-slice-or-half-slice condition is an embedded submanifold with boundary of the manifold with boundary with the subspace topology and the adopting atlas.

---

Orientation

There is a list of definitions discussed so far in this site.

There is a list of propositions discussed so far in this site.

---

Main Body

---

1: Structured Description

Here is the rules of Structured Description.

Entities:
$M$: $\in \{\text{ the }{d}^{\prime }\text{ -dimensional }{C}^{\mathrm{\infty }}\text{ manifolds with boundary }\}$
$S$: $\subseteq M$
$d$: $\in \mathbb{N}$ such that $d\le d^{\prime }$
//

Statements:
$S\in \{\text{ the subsets of }M\text{ that satisfy local-slice-or-half-slice condition with }d\}$
$⟹$
$S\text{ with the subspace topology and the adopting atlas }\in \{\text{ the embedded submanifolds with boundary of }M\}$
//

---

2: Proof

Whole Strategy: Step 1: see that $S$ is Hausdorff; Step 2: see that $S$ is 2nd-countable; Step 3: see that $S$ is locally topologically closed upper half Euclidean; Step 4: see that the adapting atlas is $C^{\mathrm{\infty }}$ compatible; Step 5: see that the inclusion, $\iota :S\to M$, is a $C^{\mathrm{\infty }}$ embedding.

Step 1:

$S$ is Hausdorff, by the proposition that any subspace of any Hausdorff topological space is Hausdorff.

Step 2:

$S$ is 2nd-countable, by the proposition that any subspace of any 2nd countable topological space is 2nd countable.

Step 3:

Let us see that $S$ is locally topologically closed upper half Euclidean.

Let $s\in S$ be any.

There are an adopted chart around $s$, $(U_s\subseteq M,{\varphi }_s)$, a $J\subseteq \{1,...,d^{\prime }\}=(j_1,...,j_d)$, and a $u\in U_s$ such that $U_s\cap S=S_{J,u}(U)$ or $U_s\cap S=H_{J,u}(U)$.

Let us suppose that $U_s\cap S=S_{J,u}(U)$.

When $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}:U_s\cap S\subseteq U\to {\pi }_J({\varphi }_s(U_s\cap S))\subseteq {\mathbb{R}}^d$ is a homeomorphism from the open neighborhood of $s$ on $S$ onto the open subset of ${\mathbb{R}}^d$, as has been seen in Note for the definition of $J$-slice of chart domain with respect to point.

When $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}:U_s\cap S\subseteq U\to {\pi }_J({\varphi }_s(U_s\cap S))\subseteq {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ (according to $d^{\prime }\in J$ or $d^{\prime }\notin J$) is a homeomorphism from the open neighborhood of $s$ on $S$ onto the open subset of ${\mathbb{H}}^d$ or ${\mathbb{R}}^d$, as has been seen in Note for the definition of $J$-slice of chart domain with respect to point.

Let us suppose that $U_s\cap S=H_{J,u}(U)$.

When $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}:U_s\cap S\subseteq U\to {\pi }_J({\varphi }_s(U_s\cap S))\subseteq {\mathbb{H}}^d$ is a homeomorphism from the open neighborhood of $s$ on $S$ onto the open subset of ${\mathbb{H}}^d$, as has been seen in Note for the definition of $J$-half-slice of chart domain with respect to point.

When $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}:U_s\cap S\subseteq U\to {\pi }_J({\varphi }_s(U_s\cap S))\subseteq {\mathbb{H}}^d$ is a homeomorphism from the open neighborhood of $s$ on $S$ onto the open subset of ${\mathbb{H}}^d$, as has been seen in Note for the definition of $J$-half-slice of chart domain with respect to point.

That means that $S$ is locally topologically closed upper half Euclidean: also any open subset of ${\mathbb{R}}^d$ is allowed, as has been mentioned in Note for the definition of locally topologically closed upper half Euclidean topological space.

Step 4:

So, let $\{(U_s\cap S\subseteq S,{\pi }_J\circ {\varphi }_s{|}_{U_s\cap S})|s\in S\}$ be an atlas for $S$.

Let us see that the atlas is $C^{\mathrm{\infty }}$ compatible.

Let $(U_s\cap S\subseteq S,{\pi }_J\circ {\varphi }_s{|}_{U_s\cap S})$ and $(U_{s^{\prime }}\cap S\subseteq S,{\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S})$ be any charts such that $(U_s\cap S)\cap (U_{s^{\prime }}\cap S)\ne \mathrm{\varnothing }$.

Let us think of ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}:{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\to {\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}((U_{s^{\prime }}\cap S)\cap (U_s\cap S))$.

We are going to apply the proposition that for any maps between any arbitrary subsets of any $C^{\mathrm{\infty }}$ manifolds with boundary $C^k$ at corresponding points, where $k$ includes $\mathrm{\infty }$, the composition is $C^k$ at the point, but the point is to carefully check that it is a legitimate chain of $C^{\mathrm{\infty }}$ maps.

Let us suppose that $U_s\cap S=S_{J,u}(U)$.

Let us suppose that $(U_s\subseteq M,{\varphi }_s)$ is an interior chart.

${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}={\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_s{|}_{U_s\cap S}$, where ${\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}:S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}\to {\mathbb{R}}^d$ is a diffeomorphism.

$({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

Let us suppose that $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart.

${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}={\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_s{|}_{U_s\cap S}$, where ${\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}:S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}\to {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ (according to $d^{\prime }\in J$ or $d^{\prime }\notin J$) is a diffeomorphism.

$({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

Let us suppose that $U_{s^{\prime }}\cap S=S_{J^{\prime },u^{\prime }}(U)$.

Let us suppose that $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart.

${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}$, where ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}:S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}\to {\mathbb{R}}^d$ is a diffeomorphism.

Let us suppose that $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart.

${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}$, where ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}:S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}\to {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ (according to $d^{\prime }\in J$ or $d^{\prime }\notin J$) is a diffeomorphism.

Let us suppose that $U_s\cap S=H_{J,u}(U)$.

Let us suppose that $(U_s\subseteq M,{\varphi }_s)$ is an interior chart.

${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}={\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_s{|}_{U_s\cap S}$, where ${\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}:H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}\to {\mathbb{H}}^d$ is a diffeomorphism.

$({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

Let us suppose that $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart.

${\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}={\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_s{|}_{U_s\cap S}$, where ${\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}:H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}\to {\mathbb{H}}^d$ is a diffeomorphism.

$({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

Let us suppose that $U_{s^{\prime }}\cap S=H_{J^{\prime },u^{\prime }}(U)$.

Let us suppose that $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart.

${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}$, where ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}:H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}\to {\mathbb{H}}^d$ is a diffeomorphism.

Let us suppose that $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart.

${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}$, where ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}:H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}\to {\mathbb{H}}^d$ is a diffeomorphism.

Now, let us suppose that $U_{s^{\prime }}\cap S=S_{J^{\prime },u^{\prime }}(U)$ and $U_s\cap S=S_{J,u}(U)$.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{R}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, by the proposition that for any maps between any arbitrary subsets of any $C^{\mathrm{\infty }}$ manifolds with boundary $C^k$ at corresponding points, where $k$ includes $\mathrm{\infty }$, the composition is $C^k$ at the point.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$ or ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{R}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$ or ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

Let us suppose that $U_{s^{\prime }}\cap S=H_{J^{\prime },u^{\prime }}(U)$ and $U_s\cap S=S_{J,u}(U)$.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{R}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, by the proposition that for any maps between any arbitrary subsets of any $C^{\mathrm{\infty }}$ manifolds with boundary $C^k$ at corresponding points, where $k$ includes $\mathrm{\infty }$, the composition is $C^k$ at the point.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{R}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{S_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d\text{ or }{\mathbb{R}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

Let us suppose that $U_{s^{\prime }}\cap S=S_{J^{\prime },u^{\prime }}(U)$ and $U_s\cap S=H_{J,u}(U)$.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, by the proposition that for any maps between any arbitrary subsets of any $C^{\mathrm{\infty }}$ manifolds with boundary $C^k$ at corresponding points, where $k$ includes $\mathrm{\infty }$, the composition is $C^k$ at the point.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$ or ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $S_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$ or ${\mathbb{R}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

Let us suppose that $U_{s^{\prime }}\cap S=H_{J^{\prime },u^{\prime }}(U)$ and $U_s\cap S=H_{J,u}(U)$.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, by the proposition that for any maps between any arbitrary subsets of any $C^{\mathrm{\infty }}$ manifolds with boundary $C^k$ at corresponding points, where $k$ includes $\mathrm{\infty }$, the composition is $C^k$ at the point.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is an interior chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{R}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is an interior chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\subseteq {\mathbb{R}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{R}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

When $(U_{s^{\prime }}\subseteq M,{\varphi }_{s^{\prime }})$ is a boundary chart and $(U_s\subseteq M,{\varphi }_s)$ is a boundary chart, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}={\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}\circ ({\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)})\circ ({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$.

But ${\pi }_{J^{\prime }}{|}_{H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}$ is $C^{\mathrm{\infty }}$ from $H_{J^{\prime },{\varphi }_{s^{\prime }}(u^{\prime })}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^d$, ${\varphi }_{s^{\prime }}\circ {\varphi }_s^{-1}{|}_{{\varphi }_s(U_{s^{\prime }}\cap U_s)}$ is $C^{\mathrm{\infty }}$ from ${\varphi }_s(U_{s^{\prime }}\cap U_s)\subseteq {\mathbb{H}}^{d^{\prime }}$ into ${\mathbb{H}}^{d^{\prime }}$, and $({\pi }_J{|}_{H_{J,\varphi (u)}({\mathbb{R}}^{d^{\prime }})\cap {\mathbb{H}}^{d^{\prime }}}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ from ${\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))\subseteq {\mathbb{H}}^d$ into ${\mathbb{H}}^{d^{\prime }}$, so, it is $C^{\mathrm{\infty }}$ as a legitimate chain of $C^{\mathrm{\infty }}$ maps, likewise.

So, ${\pi }_{J^{\prime }}\circ {\varphi }_{s^{\prime }}{|}_{U_{s^{\prime }}\cap S}\circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}{|}_{{\pi }_J\circ {\varphi }_s((U_{s^{\prime }}\cap S)\cap (U_s\cap S))}$ is $C^{\mathrm{\infty }}$ in any case.

So, the atlas is $C^{\mathrm{\infty }}$ compatible.

So, $S$ is a $C^{\mathrm{\infty }}$ manifold with boundary.

Step 5:

Let $\iota :S\to M$ be the inclusion.

Let us see that $\iota$ is a $C^{\mathrm{\infty }}$ immersion.

Let $s\in S$ be any.

Let us choose the adopted chart, $(U_s\subseteq M,{\varphi }_s)$, and the corresponding adopting char, $(U_s\cap S\subseteq S,{\pi }_J\circ {\varphi }_s{|}_{U_s\cap S})$.

The components function, ${\varphi }_s\circ \iota \circ ({\pi }_J\circ {\varphi }_s{|}_{U_s\cap S}{)}^{-1}$ is like $:(x^{j_1},...,x^{j_d})\mapsto ({\varphi }_s(u{)}^1,...,x^{j_1},...,x^{j_d},...,{\varphi }_s(u{)}^{d^{\prime }})$, where whether the 1st component is really ${\varphi }_s(u{)}^1$ or $x^{j_1}$ and whether the last component is really ${\varphi }_s(u{)}^{d^{\prime }}$ or $x^{j_d}$ really depend on $J$, but anyway, it is $C^{\mathrm{\infty }}$, and its differential is injective, by the proposition that for any $C^{\mathrm{\infty }}$ map between any $C^{\mathrm{\infty }}$ manifolds with boundary and any corresponding charts, the components function of the differential of the map with respect to the standard bases is this, so, $\iota$ is a $C^{\mathrm{\infty }}$ immersion.

The codomain restriction of $\iota$, $\iota :S\to \iota (S)\subseteq M$, is a homeomorphism, because $S$ has the subspace topology.

So, $S$ is an embedded submanifold with boundary.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>