[proofplan] We prove the theorem by applying the three structural ingredients in the Cheeger-Gromoll argument. First, the noncompact complete manifold with nonnegative sectional curvature admits a compact totally convex core obtained from a Busemann-type convex exhaustion. Second, the boundary-stripping theorem iteratively replaces a compact totally convex set with the maximum set of its distance-to-boundary function until a compact boundaryless totally geodesic totally convex submanifold $S$ remains. Finally, the normal exponential theorem for the terminal totally convex set says that the normal exponential map of $S$ has no cut locus and is a global diffeomorphism onto $M$. [/proofplan]

[step:Apply the convex exhaustion theorem to obtain an initial compact totally convex core] Let $n = \dim M$. Since $(M,g)$ is complete, connected, noncompact, and has nonnegative [sectional curvature](/page/Sectional%20Curvature), the hypotheses of the [Cheeger-Gromoll Convex Exhaustion Theorem](/page/Cheeger-Gromoll%20Convex%20Exhaustion%20Theorem) apply. That theorem gives a compact, connected, totally convex subset $C_0 \subset M$ such that $C_0$ is nonempty and every geodesic segment in $M$ with endpoints in $C_0$ is contained in $C_0$. Here total convexity means that if $p,q \in C_0$ and $\gamma: [0,1] \to M$ is a geodesic segment with $\gamma(0)=p$ and $\gamma(1)=q$, then $\gamma([0,1]) \subset C_0$. This invocation uses exactly the global geometric assumptions in the theorem statement: completeness, connectedness, noncompactness, and nonnegative sectional curvature. [/step]

[step:Strip the boundary until a boundaryless totally geodesic totally convex submanifold remains]Define compact totally convex subsets recursively, starting from the set $C_0$ constructed above. For each compact totally convex set $C_j$, the notation $\partial C_j$ and $\dim C_j$ refers to the boundary and dimension in the Cheeger-Gromoll convex-set stratification supplied by the boundary-stripping theorem. If $C_j$ has nonempty boundary in this stratification, let $\rho_j: C_j \to [0,\infty)$ denote the distance-to-boundary function \begin{align*} \rho_j(x) = \operatorname{dist}(x, \partial C_j), \end{align*} and define \begin{align*} C_{j+1} = \{x \in C_j : \rho_j(x) = \max_{y \in C_j} \rho_j(y)\}. \end{align*} By the [Cheeger-Gromoll Boundary-Stripping Theorem](/page/Cheeger-Gromoll%20Boundary-Stripping%20Theorem), each $C_{j+1}$ is nonempty, compact, and totally convex, and its dimension is strictly smaller than the dimension of $C_j$ whenever $\partial C_j \ne \varnothing$. Since the dimensions are nonnegative integers bounded above by $n$, there exists an integer $N$ with $0 \le N \le n$ such that $C_N$ has empty boundary. Let $N$ be the least such integer, and set $S = C_N$. Then $\partial S = \varnothing$. The terminal regularity conclusion in the same boundary-stripping theorem says that a compact totally convex set with empty boundary is a smooth embedded [totally geodesic submanifold](/page/Totally%20Geodesic%20Submanifold) of $M$. Hence $S \subset M$ is compact, smooth, embedded, totally geodesic, and totally convex.[/step]

[guided]We now explain why the iterative construction is legitimate and why it must stop. At stage $j$, the object $C_j$ is a compact totally convex subset of the given complete Riemannian manifold $(M,g)$ with $\operatorname{sec} \ge 0$. These are precisely the hypotheses required by the [Cheeger-Gromoll Boundary-Stripping Theorem](/page/Cheeger-Gromoll%20Boundary-Stripping%20Theorem): the theorem applies to compact totally convex subsets inside complete manifolds of nonnegative sectional curvature. If $C_j$ has nonempty boundary, define the distance-to-boundary function $\rho_j: C_j \to [0,\infty)$ by \begin{align*} \rho_j(x) = \operatorname{dist}(x, \partial C_j). \end{align*} Because $C_j$ is compact and $\rho_j$ is continuous, $\rho_j$ attains a maximum on $C_j$. Therefore the set \begin{align*} C_{j+1} = \{x \in C_j : \rho_j(x) = \max_{y \in C_j} \rho_j(y)\} \end{align*} is nonempty. The boundary-stripping theorem further states that this maximum set is compact and totally convex, and that the dimension strictly decreases when passing from $C_j$ to $C_{j+1}$. The strict dimension drop is the termination mechanism. Since $\dim C_0 \le n = \dim M$ and dimensions cannot decrease indefinitely through nonnegative integers, there is a least integer $N$ with $0 \le N \le n$ such that $C_N$ has empty boundary. Define $S = C_N$. The terminal regularity part of the theorem then converts this convex set into geometry: a compact totally convex set with empty boundary is not merely a closed subset, but a smooth embedded [totally geodesic submanifold](/page/Totally%20Geodesic%20Submanifold) of $M$. Thus $S$ is the desired compact totally geodesic totally convex candidate for the soul.[/guided]

[step:Apply the normal exponential theorem to identify the whole manifold with the normal bundle] Let $\nu(S)$ denote the [normal bundle](/page/Normal%20Bundle) of the embedded submanifold $S \subset M$, and let $\pi: \nu(S) \to S$ denote its bundle projection. Define the [normal exponential map](/page/Normal%20Exponential%20Map) \begin{align*} \exp^\perp: \nu(S) &\to M \\ v &\mapsto \exp_{\pi(v)}(v). \end{align*} The set $S$ is compact, totally geodesic, and totally convex, and it was obtained as the terminal set in the Cheeger-Gromoll boundary-stripping process. Hence the hypotheses of the [Cheeger-Gromoll Normal Exponential Theorem](/page/Cheeger-Gromoll%20Normal%20Exponential%20Theorem) apply. That theorem states that $S$ has empty normal cut locus and that $\exp^\perp$ is a smooth bijection with smooth inverse from $\nu(S)$ onto $M$. Therefore \begin{align*} \exp^\perp: \nu(S) \to M \end{align*} is a diffeomorphism. The set $S$ is connected: if $p,q \in S$, then completeness of $(M,g)$ gives a minimizing geodesic segment $\gamma: [0,1] \to M$ from $p$ to $q$, and total convexity of $S$ implies $\gamma([0,1]) \subset S$. Since $S$ is compact, connected, embedded, totally geodesic, and totally convex, and since its normal exponential map is a global diffeomorphism, $S$ is a soul of $M$. Consequently $M$ is diffeomorphic to the total space of the normal bundle $\nu(S)$, as claimed. [/step]