Compound mass is well-defined and additive

Let $E$ be any finite subset of $X$ containing $\mathrm{supp}(c)$. On $E\setminus \mathrm{supp}(c)$ the function is zero, so the finite sum over $E$ equals the finite sum over $\mathrm{supp}(c)$ by [F2]. If $E$ and $E^{\mathrm{\prime }}$ both contain the support, compare each sum to the sum over the finite union $E\cup E^{\mathrm{\prime }}$; hence the value is independent of the chosen finite summation set.

The support of $c+d$ is contained in the finite union of the supports of $c$ and $d$. Sum over that union; distributivity in [F2] gives $m(c+d)=m(c)+m(d)$, since zero terms outside each individual support contribute nothing by step 1.1. The support of $tc$ equals that of $c$ for $t>0$, and scalar linearity of the finite sum gives $m(tc)=tm(c)$. For $t=0$, $tc=0$ and both $m(tc)$ and $tm(c)$ are zero. The empty sum is zero, so $m(0)=0$.

The support of $e_x$ is the singleton $\{x\}$, whose one summand is $1$, so the recursion in [F2] gives $m(e_x)=0+1=1$. If $m(c)=0$, sum its nonnegative coefficients over its finite support. Clause 4 in [F2] forces every summand to be zero; coefficients off the support are also zero, hence $c=0$. Conversely $c=0$ has zero mass by step 2.1. Thus all the claimed mass identities hold, including the empty and unit-state cases.