# Moving a union of functions with disjoint domains

I will denote $(\lambda x\in D: f(x)) = \{(x;f(x))\,|\,x\in D\}$ for every set $D$ and a form $f$ dependent on the variable $x$.

For a function $z$ and a function $a$ we define $$\operatorname{Move} ( z ; a ) = \lambda x \in \left\{ c \in U^{\operatorname{im} a} \, | \, c \circ a \in \operatorname{dom} z \right\} : z \left( x \circ a \right)$$ where $U$ is a big enough set (e.g. a Grothendieck universe).

See Modifying every argument of a multivariable function for a background of this formula.

I want to find a nice proof of the following statement:

Conjecture Let $\gamma$ is a set of functions with disjoint domains. Then $$\operatorname{Move} \left( \bigcup \gamma ; a \right) = \bigcup_{g \in \gamma} \operatorname{Move} \left( g ; a \right) .$$

-

For simplicity we shall write $D(z;a)=\left\lbrace c\in U^{\operatorname{im}a}|\text{ }c \circ a\in\operatorname{dom}z\right\rbrace$.
We will show that $\operatorname{Move}(\bigcup\gamma;a)\subseteq\bigcup_{g\in\gamma}\operatorname{Move}(g;a)$ and $\operatorname{Move}(\bigcup\gamma;a)\supseteq\bigcup_{g\in\gamma}\operatorname{Move}(g;a)$, thus establishing the needed equality.
To see that $\operatorname{Move}(\bigcup\gamma;a)\subseteq\bigcup_{g\in\gamma}\operatorname{Move}(g;a)$, let $p\in\operatorname{Move}(\bigcup\gamma;a)$. Then $p=(x,(\bigcup\gamma)(x\circ a))$ for some $x\in D(\bigcup\gamma;a)$. (Note that $\bigcup\gamma$ is a function, since it is a union of functions with disjoint domains.) This means that $x\circ a\in\operatorname{dom}\bigcup\gamma$ so there must exist a $g_0\in\gamma$ such that $x\circ a\in\operatorname{dom}g_0$. (This is because $\operatorname{dom}\bigcup\gamma=\bigcup_{g\in\gamma}\operatorname{dom}g$.) Therefore $(\bigcup\gamma)(x\circ a)=g_0(x\circ a)$ and $x\in D(g_0;a)$ which shows that $p\in\operatorname{Move}(g_0;a)$ and thus that $p\in\bigcup_{g\in\gamma}\operatorname{Move}(g;a)$.
In the other direction, let $p\in\bigcup_{g\in\gamma}\operatorname{Move}(g;a)$. Then $p\in\operatorname{Move}(g_0;a)$ for some $g_0\in\gamma$. Therefore $p=(x,g_0(x\circ a))$ for some $x\in D(g_0;a)$. This means that $x\circ a\in\operatorname{dom}g_0\subseteq\operatorname{dom}(\bigcup\gamma)$, so we have that $x\in D(\bigcup\gamma;a)$ and $g_0(x\circ a)=(\bigcup\gamma)(x\circ a)$, which means $p\in\operatorname{Move}(\bigcup\gamma;a)$ and this concludes the proof.