On commence par le cas où est un espace affine . On utilise le produit scalaire canonique sur , vu comme champ de produits scalaires sur . Dans ce cas est isomorphe au sous-fibré de car pour tout dans . De plus on a une application définie par . Pour tout dans , la différentielle de en vaut l’identité. Elle reste donc inversible au voisinage de la section nulle. Le théorème d’inversion locale garantit que est localement injective au voisinage de la section nulle. Il reste à montrer qu’elle l’est globalement (toujours au voisinage de la section nulle). Supposons par l’absurde qu’il existe deux suite et avec et telles que pour tout mais . Par compacité de , on peut supposer que converge vers un certain . Comme et tendent vers zéro, tend aussi vers . Cela contredit l’injectivité de au voisinage de .

On démontre maintenant le cas général. Le théorème 3 fournit ¹ un plongement de dans . On peut alors munir chaque , vu comme sous-espace vectoriel de , de la restriction du produit scalaire canonique de . On alors un isomorphisme entre et . Soit la projection d’un voisinage tubulaire de fournit par la première partie de la démonstration. On définit par , qui est bien définit si est assez petit pour que soit dans . Le reste de la démonstration est complètement analogue au cas .

Soit une application continue entre deux variétés et . Le théorème 3 permet de supposer que est une sous-variété de . Soit la projection d’un voisinage tubulaire de fournit par le théorème 4.

Soit un atlas fini de et une partition de l’unité subordonnée à cet atlas. Chaque application est une application continue de dans et est compact. Soit une suite de fonctions lisses sur convergeant uniformément vers sur . On pose . Cette application est bien définie car s’annule là où n’est pas défini. On convient alors que le produit des deux est nul. Ainsi est une application lisse définie sur tout . Puisque les sont à valeur dans et de somme 1, on a l’estimée :

La somme sur ne comportant qu’un nombre fini de termes, on a bien la convergence uniforme de vers . De même l’homotopie converge vers uniformément en . En particulier les sont à valeur dans le voisinage tubulaire de pour assez grand et l’homotopie est à valeur dans . Comme était déjà à valeurs dans , et l’uniforme continuité de sur un voisinage compact de montre que tous les convergent vers quand tend vers l’infini, uniformément en .

Le cas où était déjà lisse au voisinage d’un compact est laissée en exercice.