Set theory pertaining to category theory and functional programming
The notation $f:E\times F \to G$ means that $f$ is a function that needs two arguments, one from $E$, one from $F$, and the image is in $G$.
This is how the function $\text{Union}$ is defined: the two arguments $A$, $B$ are in $\mathcal{P}(X)$ and the image $\text{Union}(A, B) = A\cup B$ is in $\mathcal{P}(X)$.