Sum of a Nonnegative Function over an Arbitrary Set

Let $A$ be a set and let $f:A\to[0,\infty)$ be a function with values in the nonnegative real numbers. For a nonempty finite subset $F\subseteq A$, $\sum_{x\in F}f(x)$ denotes the sum over the finite index set $F$ of the restriction of $f$ to $F$, and $\sum_{x\in\emptyset}f(x)=0$.

The sum of $f$ over $A$ is the element

of the extended half-line $[0,\infty]$ of Measure, Measure Space, and Probability Measure, defined as follows: if the set $\{\sum_{x\in F}f(x):\ F\subseteq A\text{ finite}\}$ of real numbers (which contains $0$) is bounded above, then $\sum_{x\in A}f(x)$ is its least upper bound; otherwise $\sum_{x\in A}f(x)=\infty$.