Is the image of a smooth homeomorphism diffeomorphic to the domain?

While I am quite sure I had seen this question before on MSE (and that I even answered it), after 20 minutes searching I could not find a duplicate. Maybe it was removed. So, here is an answer.

Proposition. Suppose that $X, Y$ are smooth 7-dimensional manifolds homeomorphic to $S^7$. Then there exists a smooth homeomorphism $X\to Y$.

At the same time, there are 28 diffeomorphism classes of such manifolds (Milnor's exotic spheres). Hence, you get examples of smooth homeomorphisms between non-diffeomorphic manifolds.

Let's prove the proposition. Milnor proved that all manifolds $X, Y$ as above are obtained by gluing two $7$-dimensional balls via a diffeomorphism of their boundaries. Thus, we only need to prove:

Lemma. Let $f: S^6\to S^6$ be a diffeomorphism. Then $f$ extends to a smooth homeomorphism $F: B^7\to B^7$ of the closed 7-dimensional unit ball. Moreover $F$ can be chosen to be a diffeomorphism away from the origin.

Proof. Let $\phi(r), r\in [0,1]$, be a smooth strictly monotonic function such that $\phi(0)=0, \phi(1)=1$ and the derivatives of all orders of $\phi$ vanish at $0$ and $\phi'(r)\ne 0$ for all $r\ne 0$. I will be using the polar coordinates $(r, \theta)$ on $B^7$, where $r\in [0,1]$, $\theta\in S^6$. Then the desired extension of $f$ is given by the formula $$ F(r,\theta)=(\phi(r), f(\theta)). $$
qed

Edit. I found an answer by Greg Kuperberg here to a similar MO question. Greg claims even more, namely that if two smooth manifolds are PL-equivalent then there is a smooth homeomorphisms between them. However, I could not follow his argument.