Il s’agit d’une conséquence du théorème de Sard et d’une observation d’algèbre linéaire triviale :

Soit la projection de sur . Par hypothèse de transversalité, est une sous-variété de et, pour tout dans , est surjective. D’après le théorème de Sard, presque tout dans est valeur régulière de la restriction à de la projection . Pour un tel , est surjective. Or donc le lemme d’algèbre linéaire montre que est transversale sur .

Soit l’application fournit par le lemme 7. On note . L’application de dans définie par est une submersion puisque, en tout , sa différentielle restreinte à est déjà surjective. Ainsi cette application est transversale sur et la proposition 5 assure que, pour presque tout , est transversale sur . On pose alors pour un petit.

L’idée consiste à empiler des translations dans toutes les directions dans des cartes de . Soit un atlas fini de et des ouverts inclus dans l’intérieur des qui recouvrent encore . Soit à support compact qui vaut un sur . Sur chaque et pour chaque vecteur dans on considère le champ de vecteur tronqué . Il est à support compact, coïncide avec sur et s’annule partout si est nul. On note son flot au temps . On remarque que, pour tout dans , la dérivée de par rapport à est l’identité puisque, pour assez petit, . Par ailleurs est à support dans . On peut donc poser

puis où est le nombre de cartes. Chaque est un difféomorphisme comme composée de difféomorphismes et . De plus chaque est une submersion en l’origine car il existe tel que contienne et la dérivée partielle de en par rapport à est surjective (c’est la différentielle de en ).

L’ensemble des tels que soit une submersion en est un ouvert de . Donc, pour chaque , il existe un ouvert de et un rayon tel que soit inclus dans . Par compacité de , on peut recouvrir par un nombre fini de et est dans pour tout . Comme est difféomorphe à , le lemme est démontré.