\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、のサブセット（部分集合）でローカル-スライス-または-ハーフ-スライス条件を満たすものは、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、である、サブスペース（部分空間）トポロジーおよびアダプティングアトラスを持って、ことの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、のサブセット（部分集合）でローカル-スライス-または-ハーフ-スライス条件を満たすものの定義を知っている。
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、のエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、の定義を知っている。
- 読者は、ローカルにトポロジカルにクローズド（閉）上半面ユークリディアントポロジカルスペース（空間）の定義を知っている。
- 読者は、任意のハウスドルフトポロジカルスペース（空間）の任意のサブスペース（部分空間）はハウスドルフであるという命題を認めている。
- 読者は、任意のセカンドカウンタブル（可算）トポロジカルスペース（空間）の任意のサブスペース（部分空間）はセカンドカウンタブル（可算）であるという命題を認めている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題を認めている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たち間の任意の\(C^\infty\)マップ（写像）および任意の対応するチャートたちに対して、当該マップ（写像）のディファレンシャルの、スタンダード（標準）ベーシス（基底）たちに関するコンポーネントたちファンクション（関数）はこれであるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、の任意のサブセット（部分集合）でローカル-スライス-または-ハーフ-スライス条件を満たすものは、当該マニフォールド（多様体）、バウンダリー（境界）付き、のエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、である、サブスペース（部分空間）トポロジーおよびアダプティングアトラスを持って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M\): \(\in \{\text{ 全ての } d' \text{ -ディメンショナル（次元） } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち } \}\)
\(S\): \(\subseteq M\)
\(d\): \(\in \mathbb{N}\)で\(d \le d'\)を満たすもの
//
ステートメント（言明）たち:
\(S \in \{M \text{ の } d \text{ でのローカル-スライス-または-ハーフ-スライス条件を満たす全てのサブセット（部分集合）たち }\}\)
\(\implies\)
\(S \text{ でサブスペース（部分空間）トポロジーおよびアダプティングアトラスを持つもの } \in \{M \text{ の全てのエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、たち }\}\)
//
2: 証明
全体戦略: ステップ1: \(S\)はハウスドルフであることを見る; ステップ2: \(S\)はセカンドカウンタブル（可算）であることを見る; ステップ3: \(S\)はローカルにトポロジカルにクローズド（閉）上半面ユークリディアンであることを見る; ステップ4: 当該アダプティングアトラスは\(C^\infty\)コンパチブル（互換）であることを見る; ステップ5: 当該インクルージョン（封入）\(\iota: S \to M\)は\(C^\infty\)エンベディング（埋め込み）であることを見る。
ステップ1:
\(S\)はハウスドルフである、任意のハウスドルフトポロジカルスペース（空間）の任意のサブスペース（部分空間）はハウスドルフであるという命題によって。
ステップ2:
\(S\)はセカンドカウンタブル（可算）である、任意のセカンドカウンタブル（可算）トポロジカルスペース（空間）の任意のサブスペース（部分空間）はセカンドカウンタブル（可算）であるという命題によって。
ステップ3:
\(S\)はローカルにトポロジカルにクローズド（閉）上半面ユークリディアンであることを見よう。
\(s \in S\)を任意のものとしよう。
以下を満たす、\(s\)の周りのあるアダプテッドチャート\((U_s \subseteq M, \phi_s)\)、ある\(J \subseteq \{1, ..., d'\} = (j_1, ..., j_d)\)、ある\(u \in U_s\)、つまり、\(U_s \cap S = S_{J, u} (U)\)または\(U_s \cap S = H_{J, u} (U)\)、がある。
\(U_s \cap S = S_{J, u} (U)\)であると仮定しよう。
\((U_s \subseteq M, \phi_s)\)がインテリア（内部）チャートである時、\(\pi_J \circ \phi_s \vert_{U_s \cap S}: U_s \cap S \subseteq U \to \pi_J (\phi_s (U_s \cap S)) \subseteq \mathbb{R}^d\)は\(s\)の\(S\)上における当該オープンネイバーフッド（開近傍）から\(\mathbb{R}^d\)の当該オープンサブセット（開部分集合）の上へのホメオモーフィズム（位相同形写像）である、チャートドメイン（定義域）の、ポイントに関する\(J\)-スライスの定義に対する"注"の中に見られるとおり。
\((U_s \subseteq M, \phi_s)\)がバウンダリー（境界）チャートである時、\(\pi_J \circ \phi_s \vert_{U_s \cap S}: U_s \cap S \subseteq U \to \pi_J (\phi_s (U_s \cap S)) \subseteq \mathbb{H}^d \text{ または } \mathbb{R}^d\)（\(d' \in J\)か\(d' \notin J\)かに応じて）は、\(s\)の\(S\)上における当該オープンネイバーフッド（開近傍）から\(\mathbb{H}^d\)または\(\mathbb{R}^d\)の当該オープンサブセット（開部分集合）の上へのホメオモーフィズム（位相同形写像）である、チャートドメイン（定義域）の、ポイントに関する\(J\)-スライスの定義に対する"注"に見られるとおり。
\(U_s \cap S = H_{J, u} (U)\)であると仮定しよう。
\((U_s \subseteq M, \phi_s)\)がインテリア（内部）チャートである時、\(\pi_J \circ \phi_s \vert_{U_s \cap S}: U_s \cap S \subseteq U \to \pi_J (\phi_s (U_s \cap S)) \subseteq \mathbb{H}^d\)は\(s\)の\(S\)上における当該オープンネイバーフッド（開近傍）から\(\mathbb{H}^d\)の当該オープンサブセット（開部分集合）の上へのホメオモーフィズム（位相同形写像）である、チャートドメイン（定義域）、のポイントに関する\(J\)-ハーフ-スライスの定義に対する"注"の中に見られるとおり。
\((U_s \subseteq M, \phi_s)\)がバウンダリー（境界）チャートである時、\(\pi_J \circ \phi_s \vert_{U_s \cap S}: U_s \cap S \subseteq U \to \pi_J (\phi_s (U_s \cap S)) \subseteq \mathbb{H}^d\)は、\(s\)の\(S\)上における当該オープンネイバーフッド（開近傍）から\(\mathbb{H}^d\)の当該オープンサブセット（開部分集合）の上へのホメオモーフィズム（位相同形写像）である、チャートドメイン（定義域）、のポイントに関する\(J\)-ハーフ-スライスの定義に対する"注"に見られるとおり。
それが意味するのは、\(S\)はローカルにトポロジカルにクローズド（閉）上半面ユークリディアンであること: \(\mathbb{R}^d\)の任意のオープンサブセット（開部分集合）も許される、ローカルにトポロジカルにクローズド（閉）上半面ユークリディアントポロジカルスペース（空間）の定義に対する"注"内に見られるとおり。
ステップ4:
そこで、\(\{(U_s \cap S \subseteq S, \pi_J \circ \phi_s \vert_{U_s \cap S}) \vert s \in S\}\)を\(S\)に対するアトラスとしよう。
当該アトラスは\(C^\infty\)コンパチブル（互換）であることを見よう。
\((U_s \cap S \subseteq S, \pi_J \circ \phi_s \vert_{U_s \cap S})\)および\((U_{s'} \cap S \subseteq S, \pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S})\)を、\((U_s \cap S) \cap (U_{s'} \cap S) \neq \emptyset\)を満たす任意のチャートたちとしよう。
\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}: \pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \to \pi_{J'} \circ \phi_{s'} ((U_{s'} \cap S) \cap (U_s \cap S))\)のことを考えよう。
私たちは、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題を適用する、しかし、要点は、それが\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）であることを注意深くチェックすることである。
\(U_s \cap S = S_{J, u} (U)\)であると仮定しよう。
\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートであると仮定しよう。
\(\pi_J \circ \phi_s \vert_{U_s \cap S} = \pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})} \circ \phi_s \vert_{U_s \cap S}\)、ここで、\(\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})}: S_{J, \phi (u)} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'} \to \mathbb{R}^d\)はディフェオモーフィズムである。
\((\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートであると仮定しよう。
\(\pi_J \circ \phi_s \vert_{U_s \cap S} = \pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_s \vert_{U_s \cap S}\)、ここで、\(\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}: S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'} \to \mathbb{H}^d \text{ or } \mathbb{R}^d\)（\(d' \in J\)か\(d' \notin J\)かに応じて）はディフェオモーフィズムである。
\((\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
\(U_{s'} \cap S = S_{J', u'} (U)\)であると仮定しよう。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャートであると仮定しよう。
\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S}\)、ここで、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}: S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'} \to \mathbb{R}^d\)はディフェオモーフィズムである。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであると仮定しよう。
\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S}\)、ここで、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}: S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'} \to \mathbb{H}^d \text{ または } \mathbb{R}^d\)（\(d' \in J\)か\(d' \notin J\)かに応じて）はディフェオモーフィズムである。
\(U_s \cap S = H_{J, u} (U)\)であると仮定しよう。
\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートであると仮定しよう。
\(\pi_J \circ \phi_s \vert_{U_s \cap S} = \pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})} \circ \phi_s \vert_{U_s \cap S}\)、ここで、\(\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})}: H_{J, \phi (u)} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'} \to \mathbb{H}^d\)はディフェオモーフィズムである。
\((\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートであると仮定しよう。
\(\pi_J \circ \phi_s \vert_{U_s \cap S} = \pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_s \vert_{U_s \cap S}\)、ここで、\(\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}: H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'} \to \mathbb{H}^d\)はディフェオモーフィズムである。
\((\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
\(U_{s'} \cap S = H_{J', u'} (U)\)であると仮定しよう。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャートであると仮定しよう。
\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S}\)、ここで、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}: H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'} \to \mathbb{H}^d\)はディフェオモーフィズムである。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであると仮定しよう。
\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S}\)、ここで、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}: H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'} \to \mathbb{H}^d\)はディフェオモーフィズムである。
さて、\(U_{s'} \cap S = S_{J', u'} (U)\)および\(U_s \cap S = S_{J, u} (U)\)であると仮定しよう。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{R}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題によって。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)または\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{R}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャート であり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d \text{ または } \mathbb{R}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)または\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d \text{ または } \mathbb{R}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\(U_{s'} \cap S = H_{J', u'} (U)\)および\(U_s \cap S = S_{J, u} (U)\)と仮定しよう。
\((U_{s'} \subseteq M, \phi_{s'})\)ははインテリア（内部）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{R}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題によって。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{R}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャート であり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d \text{ or } \mathbb{R}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{S_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d \text{ または } \mathbb{R}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\(U_{s'} \cap S = S_{J', u'} (U)\)および\(U_s \cap S = H_{J, u} (U)\)であると仮定しよう。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{R}^{d'}\)のの中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題によって。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)または\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャート であり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(S_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)または\(\mathbb{R}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\(U_{s'} \cap S = H_{J', u'} (U)\)および\(U_s \cap S = H_{J, u} (U)\)であると仮定しよう。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題によって。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はインテリア（内部）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'})})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はインテリア（内部）チャート であり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'})}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \subseteq \mathbb{R}^{d'}\)から\(\mathbb{H}^d\)の中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{R}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
\((U_{s'} \subseteq M, \phi_{s'})\)はバウンダリー（境界）チャートであり\((U_s \subseteq M, \phi_s)\)はバウンダリー（境界）チャートである時、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)} \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))} = \pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}} \circ (\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}) \circ (\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)。
しかし、\(\pi_{J'} \vert_{H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}}\)は、\(H_{J', \phi_{s'} (u')} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'} \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^d\)中へ\(C^\infty\)であり、\(\phi_{s'} \circ \phi_s^{-1} \vert_{\phi_s (U_{s'} \cap U_s)}\)は、\(\phi_s (U_{s'} \cap U_s) \subseteq \mathbb{H}^{d'}\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)であり、\((\pi_J \vert_{H_{J, \phi (u)} (\mathbb{R}^{d'}) \cap \mathbb{H}^{d'}})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は、\(\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S)) \subseteq \mathbb{H}^d\)から\(\mathbb{H}^{d'}\)の中へ\(C^\infty\)である、したがって、それは\(C^\infty\)である、\(C^\infty\)マップ（写像）たちの妥当なチェーン（連鎖）として、同様に。
したがって、\(\pi_{J'} \circ \phi_{s'} \vert_{U_{s'} \cap S} \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1} \vert_{\pi_J \circ \phi_s ((U_{s'} \cap S) \cap (U_s \cap S))}\)は\(C^\infty\)である、どのケースにおいても。
したがって、アトラスは\(C^\infty\)コンパチブル（互換）である。
したがって、\(S\)は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、である。
ステップ5:
\(\iota: S \to M\)を当該インクルージョン（封入）としよう。
\(\iota\)は\(C^\infty\)イマージョンであることを見よう。
\(s \in S\)を任意のものとしよう。
アダプテッドチャート\((U_s \subseteq M, \phi_s)\)および対応するアダプティングチャート\((U_s \cap S \subseteq S, \pi_J \circ \phi_s \vert_{U_s \cap S})\)を選ぼう。
当該コンポーネントたちファンクション（関数）\(\phi_s \circ \iota \circ (\pi_J \circ \phi_s \vert_{U_s \cap S})^{-1}\)は、\(: (x^{j_1}, ..., x^{j_d}) \mapsto (\phi_s (u)^1, ..., x^{j_1}, ..., x^{j_d}, ..., \phi_s (u)^{d'})\)のようである、ここで、第1コンポーネントが本当には\(\phi_s (u)^1\)であるか\(x^{j_1}\)であるかおよび最後のコンポーネントが本当には\(\phi_s (u)^{d'}\)であるか\(x^{j_d}\)であるかは\(J\)に依存する、しかし、いずれにせよ、それは\(C^\infty\)であり、そのディファレンシャルはインジェクティブ（単射）である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たち間の任意の\(C^\infty\)マップ（写像）および任意の対応するチャートたちに対して、当該マップ（写像）のディファレンシャルの、スタンダード（標準）ベーシス（基底）たちに関するコンポーネントたちファンクション（関数）はこれであるという命題によって、したがって、\(\iota\)は\(C^\infty\)イマージョンである。
\(\iota\)のコドメイン（余域）リストリクション（制限）\(\iota: S \to \iota (S) \subseteq M\)はホメオモーフィズム（位相同形写像）である、なぜなら、\(S\)はサブスペース（部分空間）トポロジーを持つ。
したがって、\(S\)はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、である。
