Operations over the Finite Images of Maps, and the Summands of the Simple Integral

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, maps and their values are as in Sets and Maps: Ordinary Notation (v), finite sets are as in Finite Sets (i), and for a map $s$ from a set $X$ to a set $T$, $s[X]$ is the image of $X$ under $s$, a subset of $T$, and $s^{-1}(B)$ is the preimage of a set $B$ under $s$.

(i) Let $X$, $T$ and $Y$ be sets, let $\ast$ be an associative and commutative binary operation on $Y$ with a neutral element $e$, let $A$ be a set of maps from $X$ to $T$ such that $s[X]$ is finite for every $s\in A$, and let $G:A\times T\to Y$ be a map. There is exactly one map $I:A\to Y$ with

$$I(s)=\mathop{\ast}\limits_{c\in s[X]}G(s,c)\qquad\text{for every }s\in A,$$

where, for $s\in A$, the right-hand side is the operation over the finite set $s[X]$, as in Sums and Products over a Finite Set and over an Interval (i) and Sums and Products over a Finite Set and over an Interval (ii), of the map $c\mapsto G(s,c)$ from $s[X]$ to $Y$; when $\ast$ is written $+$, it is the sum of Sums and Products over a Finite Set and over an Interval (v).

(ii) Let $(X,\mathcal{F})$ be a measurable space, let $\mu$ be a measure on $(X,\mathcal{F})$, and let $A$ be a set of maps from $X$ to $[0,\infty]$ such that $s^{-1}(\{c\})\in\mathcal{F}$ for every $s\in A$ and every $c\in[0,\infty]$. There is exactly one map $G:A\times[0,\infty]\to[0,\infty]$ with $G(s,c)=c\cdot\mu(s^{-1}(\{c\}))$ for all $s\in A$ and $c\in[0,\infty]$, where $\cdot$ is the product on $[0,\infty]$.