Q:

(Proof verification) Extension Lemma for Functions on Submanifolds

There is a similar question about this lemma in Lee's book, but I wasn't really satisfied with the detail in the proposed solution.  In particular, the OP of the linked question doesn't describe how to get the smooth maps which I am calling $f_p$ below.  I am hoping someone can give critical feedback on this proof and point out where, if anywhere, I have erred. 

Lemma 5.34 (Extension Lemma for Functions on Submanifolds).  Suppose $M$ is a smooth manifold, $S\subset M$ is a smooth submanifold,
  and $f\in C^\infty(S)$.

If $S$ is embedded, then there exist a neighborhood $U$ of $S$ in $M$
  and a smooth function $\widetilde f\in C^\infty(U)$ such that $\widetilde f|_S = f$.
If $S$ is properly embedded, then the neighborhood $U$ in part (a) can be taken to be all of $M$.

Proof of 1:
Let $n = \dim S$ and $m = \dim M$. Since $S$ is embedded, each $p\in S$ is in the domain of
a slice chart $(U_p,\varphi_p)$ in $M$ such that $S\cap U_p$ is a single slice
in $U$. Since $f$
is smooth, at each $p\in S$ we can find a slice chart so that $\mathbf{f}_p:= f\circ\varphi_p^{-1}\colon \varphi_p(S\cap
U_p)\to\Bbb R$ is smooth.  Since $\varphi_p(S\cap U_p) = \{(x^1,\dots,x^n,0,\dots,0)\in
\varphi_p(U_p)\}$, and $\mathbf{f}_p$ is smooth on this set, there is a smooth extension
$\widehat f_p\colon V_p\subset\Bbb R^m\to \Bbb R$ of $\mathbf{f}_p$, where $V_p$ is an open set in $\Bbb R^m$ containing $\varphi(p)$. 
(Here is where I see a potential "bug" in this proof.  By the definition of a smooth map on $S$, the map $\mathbf{f}_p$ is "smooth."  However, since $\mathbf{f}_p$ is defined on a set that is not an open subset of $\Bbb R^n$, I believe, and please do address this point, "smooth" means that there is the extension I am calling $\widehat f_p$.)
The restriction of $\widehat f_p$ to the open set
$W_p := \varphi_p(U_p)\cap V_p $ is still smooth and gives us a map
$f_p\colon \varphi_p^{-1}(W_p)\to\Bbb R$ defined by $f_p(x) = \big(\widehat f_p|_{W_p}\big)\circ\varphi_p(x)$.
The collection of open sets $\varphi_p^{-1}(W_p)$ is an open cover of $S$,
so let $(\psi_p)_{p\in S}$ be a partition of unity subordinate to this cover.  For any $x\in U:=\bigcup_{p\in S}\varphi^{-1}(W_p)$, define $\widetilde f(x) = \sum_{p\in S}\psi_p(x)f_p(x)$. If $x\in S$, then
$$
\widetilde f(x) = \sum_{p\in S}\psi_p(x) f(x) = f(x). 
$$
Hence $\widetilde f$ is an extension of $f$. Since the collection of supports of the  $\psi_p$ is locally finite, each point in
$U$ has a neighborhood in which the sum is finite, so this defines
a smooth map since every point has a neighborhood such that $\widetilde f$ restricted
to that neighborhood is smooth.  Hence $\widetilde f\in C^\infty(U)$ is the desired
extension.  $\square$
Proof of 2: 
In this case, the only thing that changes is that $S$ is actually closed in $M$ by a lemma in Lee's book.  By appending
$M\smallsetminus S$ to the collection $\{\varphi_p^{-1}(W_p)\}$ and taking a partition of unity
$\{\psi_p: p\in S\}\cup\{\psi_0\}$ subordinate to this open cover of $M$
with $\operatorname{supp}\psi_0\subset M\smallsetminus S$, 
define $\widetilde f(x) = \psi_0(x) + \sum_{p\in S}\psi_p(x)f_p(x)$, where $f_p$ is
defined in the first part.  $\square$

A:

I heartily welcome feedback, but I believe the proof in my question works.  The first section where I thought the proof was lacking can indeed be improved.  I got the idea for the improvement from the hint to Exercise 2.3 in Lee's Riemannian Manifolds, restated here for interest:

Exercise 2.3.  Suppose $M\subset \widetilde M$ is an embedded submanifold. 
(a) If $f$ is any smooth function on $M$, show that $f$ can be extended to a smooth function on $\widetilde M$ whose restriction to $M$ is $f$. [Hint: Extend $f$ locally in slice coordinates by letting it be independent of $(x^{n+1},\dots,x^m)$, and patch that together using a partition of unity.] 

Here is the improved proof of 1:
Let $n = \dim S$. Since $S$ is embedded, each $p\in S$ is in the domain of
a slice chart $(U_p,\varphi_p)$ in $M$ such that $f|_{S\cap U_p} = f(x^1,\dots,x^n)$ and
the $x^i$ are slice coordinates.  Extend $f|_{S\cap U_p}$ to $U_p$ by setting
$f_p(x^1,\dots,x^n,x^{n+1},\dots,x^m) = f|_{S\cap U_p}(x^1,\dots,x^n)$. The map
$f_p\colon U_p\to\Bbb R$ is smooth because it is independent of its last $m-n$ coordinates
and it is smooth with respect to its first $n$ coordinates. 
The collection of open sets $U_p$ is an open cover of $S$, so let $(\psi_p)_{p\in S}$ be 
a partition of unity subordinate to this cover, and define $\widetilde f(x) = \sum_{p\in S}
\psi_p(x)f_p(x)$. If $x\in S$, then
$$
\widetilde f(x) = \sum_{p\in S}\psi_p(x) f(x) = f(x). 
$$
Hence $\widetilde f$ is an extension of $f$.
Since the collection of supports of the  $\psi_p$ is locally finite, each point in
$U$ has a neighborhood in which the sum is finite, so this defines
a smooth map since every point has a neighborhood such that $\widetilde f$ restricted
to that neighborhood is smooth.  Hence $\widetilde f\in C^\infty(U)$ is the desired
extension.  $\square$
The proof of 2 is modified by replacing $\varphi_p^{-1}(W_p)$ with $U_p$ defined in the modified proof of 1 above.  $\square$

The reason that the original proof still works is that the extensions I describe in the first proof of 1 can be taken to be the $f_p$ explicitly described in the proof in this answer.  The approach taken here simplifies some of the notation and construction of the extension $f_p$ by blurring the distinction between points $p$ in the manifold and their local coordinate representations $(x^1,x^2,x^3,\dots)$. Smoothness of the coordinate representation of $f$ is equivalent to smoothness of the actual map defined on the manifold.