Le fait fondamental est l'existence d'une fonction cloche lisse.

En composant à droite par une homothétie, on peut imposer au support d'une cloche d'être contenu dans une boule de rayon arbitrairement petit. En utilisant un atlas, on obtient donc que, pour tout point d'une variété et tout ouvert contenant , il existe une fonction positive qui est strictement positive en et dont le support est contenu dans . Une telle fonction sera appelée cloche en à support dans .

Supposons que n'est pas compacte (le cas plus facile où est compacte est laissé en exercice). Par hypothèse de -compacité dans la définition des variétés, il existe des compacts dont la réunion recouvre . On pose . Chaque est compact, et, quitte à extraire une sous-suite, est dans l'intérieur de . Pour tout dans l'adhérence de , on choisit un ouvert suffisamment petit pour être inclus dans l'un des et dans . Soit une cloche en à support dans . On pose . Les ouverts recouvrent le compact donc on peut en extraire une famille finie. L'union sur de ces ouverts fournit un recouvrement dénombrable localement fini de par des où chaque est inclus dans un et de la forme pour une fonction lisse, positive et à support dans . La condition de finitude montre que la série converge (c'est une somme finie en restriction à n'importe quel compact). La condition de recouvrement montre que la somme est partout strictement positive. On pose

qui a bien les propriétés annoncées.

Soit un atlas d'une variété compacte . Par compacité, on peut supposer que cet atlas est fini: . Le théorème 3.1 fournit une partition de l'unité subordonnée au recouvrement par les . On va tronquer les pour les rendre constantes sur des ouverts recouvrant . Comme , pour tout de , il existe tel quel . On fixe une fonction lisse qui s'annule pour et vaut un pour . On peut par exemple construire une telle fonction en composant à gauche et à droite par des applications affines une primitive de la fonction du lemme 3.2 s'annulant au voisinage de (pour ). On pose . Par construction, les sont des ouverts inclus dans les qui recouvrent , chaque est à support compact et vaut un sur . En passant des aux , on perd le contrôle de la somme mais on gagne des ouverts sur lesquels les sont constantes.

On considère sur les applications

qui sont lisses de dans et des difféomorphismes locaux sur les correspondants. Puis on considère à valeur dans . Enfin on considère de dans . Il s'agit d'une immersion car tout point de est dans un et est injective donc a fortiori aussi. Elle est injective car, si alors pour tout donc en particulier pour . Ainsi est aussi dans et l'égalité entraîne alors puis par injectivité des cartes .

Ainsi est une immersion injective. Comme est compacte, est un plongement. En effet, l'image réciproque d'un fermé de par est égale à son image directe par . Or est compact comme fermé d'un compact donc est compact donc fermé.