indexed_union

Indexed union

context	$f:I\to X$
definiendum	$\bigcup_{i\in I,\ f} X_i \equiv \bigcup \mathrm{im}(f)$

For $f=\mathrm{id}$ , the set is indexing itself and the indexed union is just the arbitrary union $\bigcup_{i\in I} X_i = \bigcup X$ .