Supposons tout d’abord que $\omega$ est de type $(n,n)$.

Insensibilité au choix des $Y_{i}$. Supposons donnée la famille $(X_{i},\lambda_{i})$, et fixons $i$. L’élément $\int_{Y_{i}}\lambda_{i}|\omega|$ de $[0;+\infty]$ et, le cas échéant, le réel $\int_{Y_{i}}\lambda_{i}\omega$ ne dépendent pas du choix de $Y_{i}$.

Pour le voir, on choisit un (autre) domaine analytique compact $(Y^{\prime}_{i})$ de $X_{i}$ qui est un voisinage de $\operatorname{supp}(\lambda_{i}\omega)$ dans $X_{i}$.

On a alors en vertu de l’assertion 2) de la proposition 3.7.2 les égalités

et les mêmes sans valeurs absolues en cas d’intégrabilité, ce qu’on souhaitait établir.

Insensibilité au choix de tout l’atlas. On suppose donné l’atlas intégral $(X_{i},\lambda_{i},Y_{i})$  ; soit $(X^{\prime}_{i},\lambda^{\prime}_{i},Y^{\prime}_{i})$ un autre atlas intégral sur $Y$ adapté à $\omega$.

On peut modifier les $Y_{i}$ (ce qui, par ce qui précède, ne change pas les intégrales en jeu) de sorte que pour tout $i$, le domaine analytique compact $Y_{i}$ tropicalise tous les $\lambda^{\prime}_{j}$ : cela provient du fait que si $i$ est fixé, presque toutes les fonctions $\lambda^{\prime}_{j}$ sont nulles sur $X_{i}$ (qui est relativement compact). De même, pour tout $j$, on modifie $Y^{\prime}_{j}$ de sorte qu’il tropicalise toutes les fonctions lisses $\lambda_{i}$. Posons $U=\bigcup X_{i}$ et $U^{\prime}=\bigcup X^{\prime}_{j}$.

Comme les $\lambda_{i}$ et les $\lambda_{j}^{\prime}$ sont à support compact (dans $U$ et $U^{\prime}$ respectivement), on les prolonge par $0$ en des fonctions lisses sur $Y$ tout entier.

Fixons $i$ et $j$. L’intégrale $\int_{Y^{\prime}_{j}}\lambda^{\prime}_{j}\mathopen{|}{\omega}\mathclose{|}$ est alors égale à $\sum_{i}\int_{Y_{i}\cap Y^{\prime}_{j}}\lambda_{i}\lambda^{\prime}_{j}\mathopen{|}{\omega}\mathclose{|}$ (notons qu’ici la somme est finie, puisque les $\lambda_{i}$ sont presque toutes nulles au voisinage du compact $Y^{\prime}_{j}$).

En effet, $\sum\lambda_{i}=1$ sur $U$. Il existe donc un voisinage analytique compact $\Omega$ de $(\operatorname{supp}\omega)\cap Y^{\prime}_{j}$ dans $Y^{\prime}_{j}$ sur lequel $\sum\lambda_{i}=1$ (notons que par compacité de $\Omega$ cette somme est finie).

En vertu de l’assertion 2) de la proposition 3.7.2, il vient

comme annoncé. On a de même pour tout couple $(i,j)$ l’égalité

On peut dès lors écrire

ce qui prouve que $\int_{X}\mathopen{|}{\omega}\mathclose{|}$ ne dépend pas pas du choix d’un l’atlas intégral adapté à $\omega$.

Lorsque $\omega$ est intégrable, l’intégrale $\int_{X}\omega$ ne dépend pas non plus des choix faits : pour le prouver, on décalque la démonstration ci-dessus en remplaçant partout $\mathopen{|}{\omega}\mathclose{|}$ par $\omega$.

La preuve du lemme lorsque $\omega$ est une $(n-1,n)$-forme est en tout point similaire à celle que l’on vient de donner pour les $(n,n)$-formes, à ceci près qu’elle se fonde sur l’assertion 2) de la proposition 3.7.3 au lieu de l’assertion 2) de la proposition 3.7.2. ∎