Soit $x\in X$. Par définition d’une forme lisse, il existe un voisinage ouvert $U_{x}$ de $x$ dans $X$, une famille $h_{x}=(h_{x,1},\ldots,h_{x,n_{x}})$ de fonctions holomorphes inversibles sur $U_{x}$, et une forme lisse $\beta_{x}$ sur $\mathbf{R}^{n_{x}}$, tels que $\alpha|_{U_{x}}=h_{x}^{*}\beta_{x}$. Par définition de la topologie de $X$, on peut supposer qu’il existe une famille finie $(\lambda_{x,1},\ldots,\lambda_{x,r_{x}})$ de fonctions analytiques sur $X$ et, pour tout $j\in\{1,\ldots,r_{x}\}$, un intervalle ouvert borné $I_{x,j}$ de $\mathbf{R}$ tels que l’ouvert $U_{x}$ soit défini par la conjonction des conditions $|\lambda_{x,j}|\in I_{x,j}$ pour $1\leq j\leq r_{x}$, et tels que chacune des $h_{x,i}$ soit la restriction à $U_{x}$ d’une fonction inversible (encore notée $h_{x,i}$) sur le domaine affinoïde $V_{x}$ de $X$ défini par la conjonction des conditions $|\lambda_{j,x}|\in\overline{I_{x,j}}$ pour $1\leq j\leq r_{x}$.

On peut en outre remplacer chaque $h_{x,i}$ par une fonction sur $V_{x}$ qui a même tropicalisation. Soit $J$ l’ensemble des indices $j$ tels que $0\notin\overline{I_{x,j}}$. L’algèbre des fonctions analytiques de la forme $h\prod_{j\in J}\lambda_{x,j}^{n_{j}}$, où $h$ est holomorphe sur $X$ et où les $n_{j}$ sont des entiers négatifs ou nuls, est dense dans l’algèbre des fonctions analytiques sur $V_{x}$. Comme la borne inférieure sur $V_{x}$ de la norme de chacune des $h_{x,i}$ est strictement positive, on peut remplacer pour tout $i$ la fonction $h_{x_{i}}$ par une fonction de la forme $h^{\prime}_{x,i}\prod_{j\in J}\lambda_{x,j}^{n_{i,j}}$, où $h^{\prime}_{x,i}$ est holomorphe sur $X$ et où les $n_{i,j}$ sont des entiers négatifs ou nuls.

Comme $X$ est compact, il admet une partie finie $S$ de $X$ telle que les $U_{x}$, pour $x\in S$, recouvrent $X$. Considérons la famille de toutes les fonctions $h_{x,i}$ et $\lambda_{x,j}$, pour $x\in S$, $1\leq i\leq n_{x}$ et $1\leq j\leq r_{x}$, et renumérotons-la de façon arbitraire en une famille $(g_{1},\dots,g_{m})$. La description explicite de $\alpha|_{U_{x}}$ donnée ci-dessus pour tout $x\in X$ assure que $(g_{1},\ldots,g_{m})$ satisfait les conclusions de la proposition. ∎